formal: CSP toolchain selection (refines/cspmchecker)

docs/quality/formal-tools-setup.md

@@ -62,8 +62,9 @@ SPIN
   - `gcc --version`
 
 CSP
-- Toolchain is not fixed yet; the runner is wired as a **non-blocking stub**.
-- To run a CSP tool locally, configure `CSP_RUN_CMD` and call `pnpm run verify:csp`.
+- Toolchain is not fixed yet; CI runs as **non-blocking stub**.
+- Local runner supports (best-effort): `CSP_RUN_CMD` → `refines` (FDR) → `cspmchecker`.
+- To run a CSP tool locally, either install a backend or configure `CSP_RUN_CMD` and call `pnpm run verify:csp`.
   - `CSP_RUN_CMD` supports `{file}` placeholder (absolute file path).
 - Example (placeholder):
   - `CSP_RUN_CMD='echo Running CSP tool on {file}' pnpm run verify:csp -- --file spec/csp/sample.cspm`

scripts/formal/tools-check.mjs

@@ -90,6 +90,10 @@ report.push({ tool: 'gcc', present: hasGcc, version: hasGcc ? shortVer('gcc', ve
 // CSP (runner configuration)
 const cspRunCmdSet = Boolean((process.env.CSP_RUN_CMD || '').trim());
 report.push({ tool: 'CSP_RUN_CMD', present: cspRunCmdSet, path: cspRunCmdSet ? 'set (command hidden)' : 'unset (set CSP_RUN_CMD to run a CSP tool)' });
+const hasRefines = has('refines');
+report.push({ tool: 'refines', present: hasRefines, version: hasRefines ? shortVer('refines', version('refines', ['--version'])) : 'n/a' });
+const hasCspmchecker = has('cspmchecker');
+report.push({ tool: 'cspmchecker', present: hasCspmchecker, version: hasCspmchecker ? shortVer('cspmchecker', version('cspmchecker', ['--version'])) : 'n/a' });
 
 // Lean4
 const hasElan = has('elan');
@@ -116,7 +120,7 @@ try {
   const spin = map['spin'] ? `yes(${vers['spin']||'n/a'})` : 'no';
   const gcc = map['gcc'] ? `yes(${vers['gcc']||'n/a'})` : 'no';
   const lean = map['lake'] ? `yes(${vers['lake']||'n/a'})` : 'no';
-  const csp = map['CSP_RUN_CMD'] ? 'configured' : 'unset';
+  const csp = map['CSP_RUN_CMD'] ? 'CSP_RUN_CMD' : (map['refines'] ? 'refines' : (map['cspmchecker'] ? 'cspmchecker' : 'unset'));
   const jv = vers['java'] || 'n/a';
   const line = [
     `tlc=${tlc?'yes':'no'}`,

scripts/formal/verify-csp.mjs

@@ -1,5 +1,9 @@
 #!/usr/bin/env node
-// Lightweight CSP runner stub: executes CSP_RUN_CMD if provided and writes a summary JSON. Non-blocking.
+// Lightweight CSP runner:
+// - If CSP_RUN_CMD is set, execute it via shell (supports {file} placeholder).
+// - Else, if FDR `refines` exists, run a typecheck (non-blocking summary).
+// - Else, if `cspmchecker` exists, run a typecheck (non-blocking summary).
+// - Else, report tool_not_available.
 import { spawnSync } from 'node:child_process';
 import fs from 'node:fs';
 import path from 'node:path';
@@ -12,6 +16,8 @@ function parseArgs(argv) {
     if (a === '--help' || a === '-h') args.help = true;
     else if (a === '--file' && next) { args.file = next; i += 1; }
     else if (a.startsWith('--file=')) { args.file = a.slice(7); }
+    else if (a === '--mode' && next) { args.mode = next; i += 1; }
+    else if (a.startsWith('--mode=')) { args.mode = a.slice(7); }
     else { args._.push(a); }
   }
   return args;
@@ -39,6 +45,20 @@ function runShell(cmd) {
   return { available: true, success: result.status === 0, status: result.status ?? 0, output };
 }
 
+function runCommand(cmd, cmdArgs, options = {}) {
+  const result = spawnSync(cmd, cmdArgs, { encoding: 'utf8', cwd: options.cwd });
+  const stdout = result.stdout ?? '';
+  const stderr = result.stderr ?? '';
+  const output = `${stdout}${stderr}`.trim();
+  if (result.error) {
+    if (result.error.code === 'ENOENT') {
+      return { available: false, status: null, output: output || (result.error.message ?? '') };
+    }
+    return { available: true, status: result.status ?? null, output: output || (result.error.message ?? '') };
+  }
+  return { available: true, status: result.status ?? 0, output };
+}
+
 function clamp(s, n = 4000) {
   const t = String(s || '');
   return t.length > n ? `${t.slice(0, n)}…` : t;
@@ -47,6 +67,8 @@ function clamp(s, n = 4000) {
 const args = parseArgs(process.argv);
 if (args.help) {
   console.log('Usage: node scripts/formal/verify-csp.mjs [--file spec/csp/sample.cspm]');
+  console.log('Options:');
+  console.log('  --mode typecheck|assertions  (default: typecheck; only affects FDR refines backend)');
   console.log('Optional: set CSP_RUN_CMD to execute a CSP tool (supports {file}).');
   process.exit(0);
 }
@@ -62,6 +84,7 @@ let ran = false;
 let status;
 let output = '';
 let exitCode = null;
+let backend = null;
 
 if (!fs.existsSync(absFile)) {
   status = 'file_not_found';
@@ -75,20 +98,51 @@ if (!fs.existsSync(absFile)) {
     exitCode = res.status;
     status = res.available ? (res.success ? 'ran' : 'failed') : 'tool_not_available';
     output = clamp(res.output || 'CSP_RUN_CMD produced no output');
+    backend = 'CSP_RUN_CMD';
+  } else if (commandExists('refines')) {
+    // FDR (commercial): allow local runs when installed.
+    const rawMode = args.mode || 'typecheck';
+    let mode = rawMode.toLowerCase();
+    if (args.mode && mode !== 'typecheck' && mode !== 'assertions') {
+      console.error(
+        `Unknown --mode value '${args.mode}'. Expected 'typecheck' or 'assertions'. Defaulting to 'typecheck'.`,
+      );
+      mode = 'typecheck';
+    }
+    const refinesArgs = (mode === 'assertions')
+      // Run all assertions in the file (best-effort). Keep output small.
+      ? ['--brief', '--quiet', '--format', 'plain', absFile]
+      // Fast path: typecheck only (safe default).
+      : ['--typecheck', '--format', 'plain', absFile];
+    const res = runCommand('refines', refinesArgs);
+    ran = res.available;
+    exitCode = res.status;
+    status = res.available ? (res.status === 0 ? 'ran' : 'failed') : 'tool_not_available';
+    output = clamp(res.output || 'refines produced no output');
+    backend = `refines:${mode}`;
+  } else if (commandExists('cspmchecker')) {
+    // libcspm/cspmchecker (OSS): typecheck-only (no refinement).
+    const res = runCommand('cspmchecker', [absFile]);
+    ran = res.available;
+    exitCode = res.status;
+    status = res.available ? (res.status === 0 ? 'ran' : 'failed') : 'tool_not_available';
+    output = clamp(res.output || 'cspmchecker produced no output');
+    backend = 'cspmchecker';
   } else {
     // Best-effort detection: actual execution depends on selected toolchain.
-    const known = ['fdr4', 'fdr', 'refines', 'cspm'];
+    const known = ['refines', 'cspmchecker', 'cspm', 'csp0', 'fdr4', 'fdr'];
     const found = known.filter((c) => commandExists(c));
     status = 'tool_not_available';
     output = found.length
-      ? `CSP tool detected (${found.join(', ')}), but CSP_RUN_CMD is not set; execution is not configured.`
-      : 'No CSP tool configured. Set CSP_RUN_CMD or install a CSP tool.';
+      ? `CSP tool detected (${found.join(', ')}), but runner supports only CSP_RUN_CMD/refines/cspmchecker. Configure CSP_RUN_CMD or install a supported backend.`
+      : 'No CSP tool configured. Set CSP_RUN_CMD, install FDR (refines), or install cspmchecker.';
   }
 }
 
 const summary = {
   tool: 'csp',
   file: path.relative(repoRoot, absFile),
+  backend,
   ran,
   status,
   exitCode,
@@ -97,5 +151,5 @@ const summary = {
 };
 fs.writeFileSync(outFile, JSON.stringify(summary, null, 2));
 console.log(`CSP summary written: ${path.relative(repoRoot, outFile)}`);
-console.log(`- file=${summary.file} status=${status}`);
+console.log(`- file=${summary.file} status=${status}${backend ? ` backend=${backend}` : ''}`);
 process.exit(0);

spec/csp/README.md

@@ -7,7 +7,35 @@ This directory contains CSP / CSPM-style specifications for concurrency/protocol
 ## Current status
 
 - CI integration is provided as a **non-blocking stub** until a concrete toolchain is selected.
-- To execute CSP checks, set `CSP_RUN_CMD` (see below) or install a supported tool and wire it in.
+- To execute CSP checks, set `CSP_RUN_CMD` (see below) or install a supported tool.
+
+## Toolchain options (local)
+
+The runner supports these backends (best-effort, in this order):
+
+1) `CSP_RUN_CMD` (shell command)
+2) FDR `refines` (typecheck)
+3) `cspmchecker` (typecheck, OSS)
+
+FDR (commercial) example:
+
+```bash
+refines --typecheck --format plain spec/csp/sample.cspm
+pnpm run verify:csp -- --file spec/csp/sample.cspm --mode typecheck
+```
+
+If your CSPM file includes FDR assertions (e.g., deadlock freedom), you can run them:
+
+```bash
+pnpm run verify:csp -- --file spec/csp/sample.cspm --mode assertions
+```
+
+`cspmchecker` example:
+
+```bash
+cspmchecker spec/csp/sample.cspm
+pnpm run verify:csp -- --file spec/csp/sample.cspm
+```
 
 ## Files
 
@@ -64,3 +92,33 @@ CSP_RUN_CMD='echo Running CSP tool on {file}' pnpm run verify:csp -- --file spec
 
 成果物:
 - `artifacts/hermetic-reports/formal/csp-summary.json`
+
+---
+
+## ツール候補（ローカル）
+
+ランナーは次のバックエンドを（利用可能なら）優先順に使用します。
+
+1) `CSP_RUN_CMD`（シェル実行）
+2) FDR `refines`（型検査）
+3) `cspmchecker`（型検査、OSS）
+
+FDR（商用）例:
+
+```bash
+refines --typecheck --format plain spec/csp/sample.cspm
+pnpm run verify:csp -- --file spec/csp/sample.cspm --mode typecheck
+```
+
+FDR の assertion（例: deadlock free）を実行したい場合:
+
+```bash
+pnpm run verify:csp -- --file spec/csp/sample.cspm --mode assertions
+```
+
+`cspmchecker` 例:
+
+```bash
+cspmchecker spec/csp/sample.cspm
+pnpm run verify:csp -- --file spec/csp/sample.cspm
+```

spec/csp/sample.cspm

@@ -1,9 +1,11 @@
--- CSPM-style sample: minimal rendezvous
+-- CSPM-style sample: minimal rendezvous (deadlock-free)
 
 channel ch : {0..1}
 
-Sender = ch!1 -> STOP
-Receiver = ch?x -> STOP
+Sender = ch!1 -> Sender
+Receiver = ch?x -> Receiver
 
-System = Sender ||| Receiver
+System = Sender [|{|ch|}|] Receiver
 
+-- FDR assertion (optional backend): deadlock freedom (Failures model)
+assert System :[deadlock free [F]]