diff --git a/.github/workflows/gcd-reference-verify.yml b/.github/workflows/gcd-reference-verify.yml index 68dbe64..08a34ee 100644 --- a/.github/workflows/gcd-reference-verify.yml +++ b/.github/workflows/gcd-reference-verify.yml @@ -8,6 +8,8 @@ on: - 'scripts/gcd_reference_regression.py' - 'scripts/live_inspection_regression.py' - 'scripts/live_session_regression.py' + - 'scripts/agent_mcp_regression.py' + - 'setup/**' - 'examples/backend/gcd/**' - 'toolchain.json' - 'tools/**' @@ -18,6 +20,8 @@ on: - 'scripts/gcd_reference_regression.py' - 'scripts/live_inspection_regression.py' - 'scripts/live_session_regression.py' + - 'scripts/agent_mcp_regression.py' + - 'setup/**' - 'examples/backend/gcd/**' - 'toolchain.json' - 'tools/**' @@ -63,12 +67,18 @@ jobs: echo "$PWD/.cache/gcd-tools/openroad/bin" >> "$GITHUB_PATH" - name: Install native Python wheels and pinned pure-Python Kepler MCP package run: | - python -m venv .cache/gcd-python - .cache/gcd-python/bin/python -m pip install --only-binary=:all: -r tools/python-requirements.txt - .cache/gcd-python/bin/python -m pip install --no-deps -r tools/kepler-formal/mcp-requirements.txt - .cache/gcd-python/bin/python -m pip check + mkdir -p .cache/agent-config-codex .cache/agent-config-claude + python setup/mcp.py configure --client codex --project .cache/agent-config-codex \ + --venv .cache/gcd-python --apply | tee .cache/gcd-tools/setup-codex.log + python setup/mcp.py configure --client claude-code --project .cache/agent-config-claude \ + --venv .cache/gcd-python --apply | tee .cache/gcd-tools/setup-claude.log .cache/gcd-python/bin/python -m pip freeze > .cache/gcd-tools/python-packages.txt echo "$PWD/.cache/gcd-python/bin" >> "$GITHUB_PATH" + - name: Agent MCP discovery and direct live-session verification + run: | + python setup/mcp.py check --venv .cache/gcd-python + python scripts/agent_mcp_regression.py --work-dir runs/agent-mcp + python scripts/live_session_regression.py --work-dir runs/live-session - name: Verify package identities and prepare immutable inputs run: | openroad -version | tee .cache/gcd-tools/openroad-version.txt @@ -95,6 +105,8 @@ jobs: path: | runs/gcd-reference/ runs/live-inspection/ + runs/agent-mcp/ + runs/live-session/ .cache/gcd-tools/*.json .cache/gcd-tools/*.txt .cache/gcd-tools/*.log diff --git a/.gitignore b/.gitignore index b1c64c6..6fd234c 100644 --- a/.gitignore +++ b/.gitignore @@ -11,3 +11,8 @@ result-* /thirdparty/ /flow_runs/ /skill_adapters/ +# Machine-specific agent setup, never shared as portable configuration. +/.codex/config.toml +/.codex/config.toml.22b-* +/.mcp.json +/.mcp.json.22b-* diff --git a/README.md b/README.md index 51f8a81..dc31fcb 100644 --- a/README.md +++ b/README.md @@ -13,6 +13,7 @@ flow/rtl/ RTL authoring and design changes examples/backend/gcd/ GCD design and independent model task examples/rtl/ RTL example conventions tools/ Shared tool skills and package installation guides +setup/ Direct MCP registration for Codex and Claude Code toolchain.json Pinned package and fixture references tests/ Fast, offline repository and example checks ``` @@ -30,7 +31,9 @@ if the inline player is unavailable. ## Start -1. Read the [package setup](tools/README.md). Kepler Formal runs through its +1. Use [agent MCP setup](setup/README.md) to expose Kepler tools directly in + Codex or Claude Code. Read the [package setup](tools/README.md) for other tools. + Kepler Formal runs through its Python-backed MCP with native wheels; OpenROAD uses Nix. No source submodules are required in 22b. 2. Choose the [backend](flow/backend/SKILL.md) or [RTL](flow/rtl/SKILL.md) flow. diff --git a/SKILL.md b/SKILL.md index 9234ad5..3ccf141 100644 --- a/SKILL.md +++ b/SKILL.md @@ -11,6 +11,9 @@ description: Coordinate open-source hardware design tools for backend optimizati - For RTL creation or changes, read [RTL](flow/rtl/SKILL.md). - Read [package setup](tools/README.md) only when a needed tool is absent or its version does not match the experiment. Check existing installations first. +- If Kepler tools are absent from the agent's own tool list, use + [agent MCP setup](setup/README.md). Installing a Python package or calling + the live helper's internal client does not register tools with the host app. Load only the tool skill relevant to the next operation. A gate-replacement task needs connectivity and replacement guidance, not constant-propagation diff --git a/scripts/agent_mcp_regression.py b/scripts/agent_mcp_regression.py new file mode 100644 index 0000000..283a89d --- /dev/null +++ b/scripts/agent_mcp_regression.py @@ -0,0 +1,116 @@ +"""Check direct agent MCP transport against the same live designs as the edit API.""" + +import argparse +import asyncio +import json +import os +from pathlib import Path +import runpy +import sys +import tempfile + + +ROOT = Path(__file__).resolve().parents[1] +sys.path.insert(0, str(ROOT)) + +from scripts.live_session_regression import LIBERTY, FIRST, SECOND, DIFFERENT +from tools.live_session import LiveDesignSession, SEC + + +async def run(work): + from mcp import ClientSession, StdioServerParameters + from mcp.client.stdio import stdio_client + + work.mkdir(parents=True, exist_ok=False) + source, library = work / "input.v", work / "cells.lib" + source.write_text('module top(input a, output y); BUF g(.A(a), .Y(y)); endmodule\n') + library.write_text(LIBERTY) + setup = runpy.run_path(str(ROOT / "setup/mcp.py")) + with LiveDesignSession(source, [library], work / "owner") as owner: + coordinates = owner.mcp_attachment() + original = owner.status()["golden_sha256"] + # The generated client entries are tested outside any real agent config. + with tempfile.TemporaryDirectory(prefix="22b-agent-config-") as temporary: + project = Path(temporary) + for client in ("codex", "claude-code"): + entry = setup["configuration"](client, Path(sys.executable)) + path = setup["config_path"](project, client) + config = setup["render_config"](None, client, "kepler-formal", entry) + setup["write_config"](path, None, config) + parsed = (setup["tomllib"].loads(path.read_text()) if client == "codex" + else json.loads(path.read_text())) + key = "mcp_servers" if client == "codex" else "mcpServers" + configured = parsed[key]["kepler-formal"] + params = StdioServerParameters(command=configured["command"], args=configured["args"], + env=setup["clean_env"](), cwd=str(work)) + with (work / f"{client}-server.log").open("w") as log: + async with stdio_client(params, errlog=log) as streams: + async with ClientSession(*streams) as agent: + await agent.initialize() + names = {tool.name for tool in (await agent.list_tools()).tools} + if not setup["REQUIRED_TOOLS"] <= names: + raise ValueError("Agent is missing direct Kepler tools") + attachment = SEC.payload(await agent.call_tool("attach_session", { + "connection_file": coordinates["connection_file"]})) + if attachment.get("session_id") != coordinates["session_id"] or attachment.get("pid") != os.getpid(): + raise ValueError("Agent attached to a different live owner") + + async def verify(label, *, different=False): + before = owner.mcp_attachment() + options = {key: before[key] for key in ("session_id", "design1", "design2")} + options.update(verification="sec", solver="kissat", max_k=32, + sec_engine="pdr", sec_encoding="dual_rail_steady", + report_skipped_outputs=True, timeout_seconds=60, + allow_boundary_mismatch=False) + result = SEC.payload(await agent.call_tool("verify_session", options)) + for key in ("session_id", "design1", "design2"): + if result.get(key) != before[key]: + raise ValueError("Proof identifies different designs") + reports = SEC.payload(await agent.call_tool("get_session_reports", { + "session_id": before["session_id"], "report_id": result["report_id"]})) + for key in ("session_id", "design1", "design2", "report_id", "verification_result"): + if reports.get(key) != result.get(key): + raise ValueError("Reports do not match this direct proof") + if owner.mcp_attachment() != before: + raise ValueError("Candidate revision changed during direct proof") + if different: + if result.get("verdict") != "different": + raise ValueError("Incorrect edit was not rejected by direct SEC") + else: + SEC.require_full(SEC.summarize(result), 1) + SEC.require_full(SEC.summarize(reports), 1) + SEC.save(work / f"{client}-{label}.json", result) + print(f"PASS: {client}: {label}", flush=True) + + if client == "codex": + await verify("initial") + for number, script in enumerate((FIRST, SECOND), 1): + SEC.require_full(owner.apply_edit(script), 1) + await verify(f"edit-{number}") + else: + # A second independent server sees the already-edited design. + await verify("existing-candidate") + try: + owner.apply_edit(DIFFERENT) + except ValueError as error: + if "counterexample" not in str(error): + raise + else: + raise ValueError("Automatic SEC accepted the incorrect edit") + await verify("counterexample", different=True) + SEC.payload(await agent.call_tool("close_session", { + "session_id": coordinates["session_id"]})) + if owner.status()["golden_sha256"] != original: + raise ValueError("Detaching agent destroyed or changed owner's designs") + if list((work / "owner").rglob("*.v")): + raise ValueError("Live verification unexpectedly exported a design") + SEC.save(work / "result.json", {"status": "passed", "direct_stdio_clients": 2, + "equivalent_edits": 2, "counterexample_rejected": True, "design_exports": 0, + "host_app_ui_tested": False}) + + +if __name__ == "__main__": + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--work-dir", type=Path, required=True) + args = parser.parse_args() + asyncio.run(run(args.work_dir.resolve())) diff --git a/setup/README.md b/setup/README.md new file mode 100644 index 0000000..7983991 --- /dev/null +++ b/setup/README.md @@ -0,0 +1,114 @@ +# Agent MCP Setup + +Install the pinned Kepler Formal MCP and register its tools **directly with +the agent app**. This is separate from the internal MCP client used by the +live-edit helper. Setup targets Codex and Claude Code, not model names. An +Ollama-backed agent needs its own MCP-capable host; Ollama alone is not configured +by this command. No model, account credentials or global agent settings change. + +## Install And Register + +From the 22b root, using Python 3.13, preview first: + +```sh +python3.13 setup/mcp.py configure --client codex +python3.13 setup/mcp.py configure --client codex --apply +# Or, for Claude Code: +python3.13 setup/mcp.py configure --client claude-code --apply +``` + +The same installer checks and reuses `.venv`, installs only missing/mismatched +pins, tests real MCP initialization, lists tools and calls Kepler's native +information tool, then writes the selected client's **project-local** config: + +| Client | Generated file | Activation | +| --- | --- | --- | +| Codex | `.codex/config.toml` | Trust the project, reload the client, check `/mcp` | +| Claude Code | `.mcp.json` | Approve the project MCP server, reload, check `/mcp` | + +Use `--venv /absolute/existing-venv` to reuse the kernel's environment, and +`--project /absolute/project` to configure a different project. An existing venv +is modified only with `--apply`; use a dedicated one if its other packages must +remain unchanged. Config entries use absolute paths to that interpreter and +this checkout's launcher, so keep both at those paths. Regenerate after moving. + +Existing unrelated configuration is preserved and backed up before changes. +An identical entry is reused; a conflicting entry stops setup before install. +Review it manually or use `--name another-name`; setup never silently replaces +an existing server. Local paths and config backups should not be committed. +The standard generated files are ignored by this repository. + +The installer uses [pinned native wheels](../tools/python-requirements.txt), +[kernel packages](../tools/session-requirements.txt) and the +[pinned pure-Python wrapper](../tools/kepler-formal/mcp-requirements.txt). +No Nix, native build or source submodule is needed for this MCP. Missing native +wheels are an error, not permission to compile. The launcher checks the package +pins on every startup. Transitive dependencies are not fully locked. + +Check an existing installation without installing or changing configuration: + +```sh +python3.13 setup/mcp.py check --venv .venv +``` + +This checks transport/tool discovery and native loading, **not** whether your +agent has approved or displayed the tools, and not circuit equivalence. In the +agent's tool list confirm `get_kepler_formal_info`, `attach_session`, +`verify_session` and `get_session_reports`. Existing user/admin settings can +override or block project settings; resolve that in the host rather than +overwriting them. Keep normal host approval controls enabled. Codex's generated +tool timeout allows a 600-second proof plus transport overhead; for other hosts +ensure their MCP call timeout also accommodates the requested proof duration. + +## Attach To The Live Designs + +Start the [persistent session](../tools/live-session.md) in a dedicated kernel +using this same environment. In that kernel: + +```python +attachment = session.mcp_attachment() +``` + +Then the **agent's registered Kepler tools**, not a new notebook MCP client, do: + +1. Call `attach_session` with `attachment["connection_file"]`. +2. Require its returned session ID to match `attachment["session_id"]`. +3. Call `verify_session` with that session ID and the returned `design1` and + `design2` native references. Set `verification="sec"`, `solver="kissat"`, + `max_k=32`, `sec_engine="pdr"`, `sec_encoding="dual_rail_steady"`, + `report_skipped_outputs=true`, `allow_boundary_mismatch=false`, and an + appropriate `timeout_seconds` (600 by default). +4. Call `get_session_reports` with the result's `report_id` and session ID. + Require the exact design pair and report identity to match. Apply the + [SEC evidence rules](../tools/kepler-formal/SKILL.md), including proof coverage. + +Use the native references as returned; golden/candidate are local roles, not +MCP aliases. Keep edits and direct proofs sequential. Recheck +`session.mcp_attachment()` after a direct proof: its revision and references +must still match the ones observed before it. A proof for an older revision +does not certify the current candidate. + +Do not read, print or upload the connection file's token. Only its path is +returned. Attachment requires the same machine/user and permission to reach +the loopback bridge; a remote or sandboxed agent may need approved access. +Do not load/reset designs through another server or bypass `session.apply_edit`. +That method still enforces script validation and automatic SEC independently +of the model. Direct tools provide additional explicit agent verification; +they do not replace that mandatory check or overwrite its recorded proof. +Detach with `close_session`; this leaves the caller's designs alive. Closing +the owner session invalidates the attachment. + +## Validation + +```sh +python -m unittest discover -s tests -v +.venv/bin/python scripts/agent_mcp_regression.py --work-dir runs/agent-mcp-check +``` + +The real regression launches the generated server entries as independent MCP +clients, attaches to the live owner, proves both cumulative edits, rejects a +counterexample and checks that detaching preserves the designs. It does not +claim to test an interactive Codex or Claude model session. + +Client formats: [Codex MCP documentation](https://developers.openai.com/codex/mcp) +and [Claude Code MCP documentation](https://code.claude.com/docs/en/mcp). diff --git a/setup/kepler_server.py b/setup/kepler_server.py new file mode 100644 index 0000000..d898770 --- /dev/null +++ b/setup/kepler_server.py @@ -0,0 +1,24 @@ +"""Agent stdio entry point: require the pinned package, then serve upstream MCP.""" + +import os +from pathlib import Path +import runpy +import sys + + +def main(): + for name in ("PYTHONPATH", "PYTHONHOME", "NAJAEDA_SRC", "EQUIVALENCE_CHECK"): + os.environ.pop(name, None) + root = Path(__file__).resolve().parents[1] + verify = runpy.run_path(str(root / "tools/kepler-formal/verify.py")) + verify["package_identity"]() + # Reserve stdout exclusively for the upstream JSON-RPC transport. + runpy.run_module("kepler_formal_mcp", run_name="__main__") + + +if __name__ == "__main__": + try: + main() + except (OSError, ValueError, ImportError) as error: + print(f"Kepler MCP setup is not ready: {error}", file=sys.stderr) + sys.exit(1) diff --git a/setup/mcp.py b/setup/mcp.py new file mode 100644 index 0000000..851692d --- /dev/null +++ b/setup/mcp.py @@ -0,0 +1,246 @@ +"""Install pinned tools and register Kepler MCP with a local agent project.""" + +import argparse +import asyncio +import importlib.metadata +import json +import os +from pathlib import Path +import re +import runpy +import subprocess +import sys +import tempfile +import tomllib +import venv + + +ROOT = Path(__file__).resolve().parents[1] +SCRIPT = Path(__file__).resolve() +LAUNCHER = SCRIPT.with_name("kepler_server.py") +REQUIRED_TOOLS = {"get_kepler_formal_info", "create_yaml_and_run_kepler_formal", + "attach_session", "verify_session", "get_session_reports"} + + +def clean_env(): + env = dict(os.environ) + for key in ("PYTHONPATH", "PYTHONHOME", "NAJAEDA_SRC", "EQUIVALENCE_CHECK"): + env.pop(key, None) + return env + + +def identity(): + pins = json.loads((ROOT / "toolchain.json").read_text()) + requirements = dict(pins["python_packages"]) + for line in (ROOT / "tools/session-requirements.txt").read_text().splitlines(): + if line and not line.startswith("#"): + name, version = line.split("==") + requirements[name] = version + versions = {} + for name in requirements: + try: + versions[name] = importlib.metadata.version(name) + except importlib.metadata.PackageNotFoundError: + versions[name] = None + pin = pins["kepler_formal_mcp"] + try: + dist = importlib.metadata.distribution("kepler-formal-mcp") + origin = json.loads(dist.read_text("direct_url.json") or "{}") + wrapper = (dist.version == pin["version"] and origin.get("url") == pin["repository"] + and origin.get("vcs_info", {}).get("commit_id") == pin["revision"]) + except (importlib.metadata.PackageNotFoundError, ValueError): + wrapper = False + return {"packages_match": versions == requirements, "wrapper_match": wrapper, + "versions": versions} + + +def run(command, *, capture=False, timeout=600): + return subprocess.run([str(arg) for arg in command], check=True, env=clean_env(), + text=True, capture_output=capture, timeout=timeout) + + +def python_in(directory): + # Do not resolve the executable symlink: Python needs the venv path. + return directory / ("Scripts/python.exe" if os.name == "nt" else "bin/python") + + +def install(directory): + python = python_in(directory) + if directory.exists(): + if not (directory / "pyvenv.cfg").is_file() or not python.is_file(): + raise ValueError("Existing environment is not a usable venv; choose another --venv") + else: + venv.EnvBuilder(with_pip=True).create(directory) + state = json.loads(run([python, "-I", SCRIPT, "identity"], capture=True).stdout) + if not state["packages_match"]: + run([python, "-I", "-m", "pip", "install", "--only-binary=:all:", + "-r", ROOT / "tools/python-requirements.txt", + "-r", ROOT / "tools/session-requirements.txt"]) + if not state["wrapper_match"]: + run([python, "-I", "-m", "pip", "install", "--no-deps", "--force-reinstall", + "-r", ROOT / "tools/kepler-formal/mcp-requirements.txt"]) + if state["packages_match"] and state["wrapper_match"]: + print("Reusing the matching pinned installation.", flush=True) + run([python, "-I", "-m", "pip", "check"]) + return python + + +def configuration(client, python): + config = {"command": str(python), "args": ["-I", str(LAUNCHER)]} + if client == "codex": + config.update(startup_timeout_sec=60, tool_timeout_sec=660) + else: + config["type"] = "stdio" + return config + + +def config_path(project, client): + return project / (".codex/config.toml" if client == "codex" else ".mcp.json") + + +def read_config(path): + if path.is_symlink() or path.parent.is_symlink(): + raise ValueError("Refusing to change a symlinked agent configuration") + return path.read_bytes() if path.exists() else None + + +def render_config(old, client, name, entry): + text = (old or b"").decode("utf-8") + if client == "codex": + data = tomllib.loads(text) + key = "mcp_servers" + else: + data = json.loads(text) if old is not None else {} + key = "mcpServers" + if not isinstance(data, dict) or not isinstance(data.get(key, {}), dict): + raise ValueError("Invalid existing MCP configuration; it was not changed") + servers = data.setdefault(key, {}) + if name in servers: + if servers[name] != entry: + raise ValueError(f"MCP server '{name}' already has different settings; " + "choose --name or review the existing entry manually") + return old + servers[name] = entry + if client == "codex": + addition = f"\n[mcp_servers.{name}]\n" + "".join( + f"{key} = {json.dumps(value)}\n" for key, value in entry.items()) + result = text + addition + if tomllib.loads(result) != data: + raise ValueError("Cannot safely extend this TOML layout; no configuration changed") + else: + result = json.dumps(data, indent=2) + "\n" + return result.encode("utf-8") + + +def write_config(path, old, new): + if old == new: + if read_config(path) != old: + raise ValueError("Agent configuration changed during setup; rerun without overwriting it") + return + path.parent.mkdir(parents=True, exist_ok=True) + # Coordinate setup invocations and reject changes since the initial read. + lock = path.with_name(path.name + ".22b-lock") + with lock.open("x"): + try: + if read_config(path) != old: + raise ValueError("Agent configuration changed during setup; rerun without overwriting it") + if old is not None: + fd, backup = tempfile.mkstemp(prefix=path.name + ".22b-backup-", dir=path.parent) + with os.fdopen(fd, "wb") as stream: + stream.write(old) + print(f"Previous config saved: {backup}", flush=True) + fd, temporary = tempfile.mkstemp(prefix=path.name + ".22b-", dir=path.parent) + try: + with os.fdopen(fd, "wb") as stream: + stream.write(new) + os.replace(temporary, path) + finally: + Path(temporary).unlink(missing_ok=True) + finally: + lock.unlink() + + +async def probe(): + from mcp import ClientSession, StdioServerParameters + from mcp.client.stdio import stdio_client + + state = identity() + if not state["packages_match"] or not state["wrapper_match"]: + raise ValueError("Environment does not match the toolchain and session pins") + sec = runpy.run_path(str(ROOT / "tools/kepler-formal/verify.py")) + with tempfile.TemporaryDirectory(prefix="22b-mcp-probe-") as work: + params = StdioServerParameters(command=sys.executable, args=["-I", str(LAUNCHER)], + env=clean_env(), cwd=work) + async with asyncio.timeout(90): + async with stdio_client(params) as streams: + async with ClientSession(*streams) as session: + await session.initialize() + names = {tool.name for tool in (await session.list_tools()).tools} + if not REQUIRED_TOOLS <= names: + raise ValueError(f"Missing MCP tools: {sorted(REQUIRED_TOOLS - names)}") + info = sec["payload"](await session.call_tool("get_kepler_formal_info", {})) + if info.get("status") != "success": + raise ValueError("Kepler Python library capability check failed") + return {"status": "ready", "tools": sorted(names), "native_import": "passed", + "host_tool_visibility": "requires host reload and approval"} + + +def check(python): + reply = run([python, "-I", SCRIPT, "probe"], capture=True, timeout=120) + result = json.loads(reply.stdout) + if result.get("status") != "ready": + raise ValueError("MCP probe did not establish readiness") + print(json.dumps(result, indent=2), flush=True) + return result + + +def main(argv=None): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("action", choices=("configure", "check", "identity", "probe")) + parser.add_argument("--client", choices=("codex", "claude-code")) + parser.add_argument("--project", type=Path, default=ROOT) + parser.add_argument("--venv", type=Path, help="Existing/new dedicated venv (default: PROJECT/.venv)") + parser.add_argument("--name", default="kepler-formal") + parser.add_argument("--apply", action="store_true", help="Install and write project config; otherwise preview only") + args = parser.parse_args(argv) + if args.action == "identity": + print(json.dumps(identity())) + return + if args.action == "probe": + print(json.dumps(asyncio.run(probe()))) + return + project = args.project.resolve(strict=True) + directory = args.venv.resolve() if args.venv else project / ".venv" + python = python_in(directory) + if args.action == "check": + check(python) + return + if not args.client: + parser.error("configure requires --client") + if not re.fullmatch(r"[A-Za-z0-9_-]+", args.name): + parser.error("--name must contain only letters, numbers, underscores and hyphens") + path = config_path(project, args.client) + entry = configuration(args.client, python) + old = read_config(path) + new = render_config(old, args.client, args.name, entry) + print(json.dumps({"client": args.client, "scope": "project", "config": str(path), + "environment": str(directory), "server": entry, + "apply": args.apply}, indent=2), flush=True) + if not args.apply: + print("Preview only. Add --apply to install, test MCP discovery, and register.") + return + install(directory) + check(python) + write_config(path, old, new) + print("Registered. Reload the agent and approve the trusted project/server. " + "Confirm Kepler tools in its MCP tool list; host visibility is not tested by this probe.") + + +if __name__ == "__main__": + try: + main() + except (OSError, ValueError, RuntimeError, subprocess.SubprocessError, ExceptionGroup) as error: + print(f"MCP setup failed: {error}", file=sys.stderr) + if isinstance(error, subprocess.CalledProcessError): + print(error.stderr or error.stdout or "", file=sys.stderr) + sys.exit(1) diff --git a/tests/test_live_session.py b/tests/test_live_session.py index 5fdbce7..414583f 100644 --- a/tests/test_live_session.py +++ b/tests/test_live_session.py @@ -81,6 +81,7 @@ def setUp(self): session._golden_ref, session._candidate_ref = dict(GOLDEN_REF), dict(CANDIDATE_REF) session._netlist = SimpleNamespace(get_top=lambda: session._candidate) session._bridge = SimpleNamespace(lock=threading.RLock(), close=Mock()) + session._bridge.connection_file = session.directory / "private-connection.json" session._session_id = "fixture-session" session._client = Mock() session._client.busy.return_value = False @@ -95,6 +96,33 @@ def setUp(self): fingerprint.start() self.addCleanup(fingerprint.stop) + def test_agent_attachment_is_a_copy_without_secrets_or_side_effects(self): + self.session._bridge.connection_file.write_text('{"token": "never-return-this"}') + self.session.proof = {"status": "proved"} + info = self.session.mcp_attachment() + self.assertEqual(info["design1"], GOLDEN_REF) + self.assertEqual(info["design2"], CANDIDATE_REF) + self.assertEqual(info["revision"], 0) + self.assertNotIn("never-return-this", json.dumps(info)) + info["design1"]["db_id"] = 200 + self.assertEqual(self.session._golden_ref, GOLDEN_REF) + self.assertEqual(self.session.proof, {"status": "proved"}) + self.session._candidate.dumpVerilog.assert_not_called() + self.session._client.call.assert_not_called() + + def test_agent_attachment_rejects_closed_busy_or_untracked_sessions(self): + self.session._closed = True + with self.assertRaises(RuntimeError): + self.session.mcp_attachment() + self.session._closed = False + self.session._pending = True + with self.assertRaises(RuntimeError): + self.session.mcp_attachment() + self.session._pending = False + self.session._candidate.signature = "untracked" + with self.assertRaises(RuntimeError): + self.session.mcp_attachment() + def test_edits_accumulate_and_sec_is_automatic(self): def edit(top): top.signature += "-edit" diff --git a/tests/test_repository.py b/tests/test_repository.py index 097c23e..8219df7 100644 --- a/tests/test_repository.py +++ b/tests/test_repository.py @@ -12,6 +12,7 @@ DOCS = [ROOT / "README.md", ROOT / "AGENTS.md", ROOT / "SKILL.md", *sorted((ROOT / "flow").rglob("*.md")), *sorted((ROOT / "tools").rglob("*.md")), + *sorted((ROOT / "setup").rglob("*.md")), *sorted((ROOT / "examples").rglob("*.md"))] diff --git a/tests/test_setup_mcp.py b/tests/test_setup_mcp.py new file mode 100644 index 0000000..8520d4f --- /dev/null +++ b/tests/test_setup_mcp.py @@ -0,0 +1,162 @@ +"""Offline setup safety and client-format checks; no host configuration writes.""" + +import importlib.util +import json +from pathlib import Path +import subprocess +import sys +import tempfile +import tomllib +import unittest +from unittest.mock import patch + + +ROOT = Path(__file__).resolve().parents[1] +SPEC = importlib.util.spec_from_file_location("mcp_setup", ROOT / "setup/mcp.py") +setup = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(setup) + + +class SetupTests(unittest.TestCase): + def setUp(self): + temp = tempfile.TemporaryDirectory() + self.addCleanup(temp.cleanup) + self.project = Path(temp.name) + self.python = self.project / "env with spaces/bin/python" + + def test_codex_preserves_existing_content_and_is_idempotent(self): + original = b'# keep this comment\nmodel = "example"\n[mcp_servers.other]\ncommand = "other"\n' + entry = setup.configuration("codex", self.python) + data = setup.render_config(original, "codex", "kepler-formal", entry) + self.assertTrue(data.startswith(original)) + parsed = tomllib.loads(data.decode()) + self.assertEqual(parsed["mcp_servers"]["other"]["command"], "other") + self.assertEqual(parsed["mcp_servers"]["kepler-formal"], entry) + self.assertEqual(setup.render_config(data, "codex", "kepler-formal", entry), data) + self.assertGreater(entry["tool_timeout_sec"], 600) + + def test_claude_preserves_other_servers_and_fields(self): + original = json.dumps({"mcpServers": {"other": {"command": "other"}}, "custom": 7}).encode() + entry = setup.configuration("claude-code", self.python) + data = setup.render_config(original, "claude-code", "kepler-formal", entry) + parsed = json.loads(data) + self.assertEqual(parsed["custom"], 7) + self.assertEqual(parsed["mcpServers"]["other"], {"command": "other"}) + self.assertEqual(parsed["mcpServers"]["kepler-formal"], entry) + self.assertEqual(entry["type"], "stdio") + self.assertEqual(setup.render_config(data, "claude-code", "kepler-formal", entry), data) + + def test_existing_entry_conflict_never_overwritten(self): + for client in ("codex", "claude-code"): + old = setup.render_config(None, client, "kepler-formal", {"command": "other"}) + with self.assertRaisesRegex(ValueError, "different settings"): + setup.render_config(old, client, "kepler-formal", setup.configuration(client, self.python)) + + def test_malformed_configs_fail(self): + for client, data in (("codex", b"broken ["), ("codex", b"mcp_servers = 1"), + ("claude-code", b"{"), ("claude-code", b"[]"), + ("claude-code", b'{"mcpServers": []}')): + with self.subTest(client=client, data=data), self.assertRaises(ValueError): + setup.render_config(data, client, "test", {}) + + def test_config_preview_does_not_install_or_write(self): + with patch.object(setup, "install") as install, patch.object(setup, "check") as check: + setup.main(["configure", "--client", "codex", "--project", str(self.project)]) + install.assert_not_called() + check.assert_not_called() + self.assertEqual(list(self.project.iterdir()), []) + + def test_apply_checks_before_writing(self): + with patch.object(setup, "install", return_value=self.python), \ + patch.object(setup, "check", side_effect=ValueError("discovery failed")): + with self.assertRaisesRegex(ValueError, "discovery failed"): + setup.main(["configure", "--client", "codex", "--project", str(self.project), "--apply"]) + self.assertFalse((self.project / ".codex").exists()) + + def test_conflict_is_checked_before_installation(self): + path = self.project / ".mcp.json" + path.write_text('{"mcpServers":{"kepler-formal":{"command":"other"}}}') + with patch.object(setup, "install") as install, self.assertRaises(ValueError): + setup.main(["configure", "--client", "claude-code", "--project", str(self.project), "--apply"]) + install.assert_not_called() + + def test_write_backups_and_noop_does_not_rewrite(self): + path = self.project / ".mcp.json" + old, new = b"{}", b'{"mcpServers":{}}' + path.write_bytes(old) + setup.write_config(path, old, new) + self.assertEqual(path.read_bytes(), new) + backup = list(self.project.glob("*.22b-backup-*")) + self.assertEqual(len(backup), 1) + self.assertEqual(backup[0].read_bytes(), old) + before = path.stat().st_mtime_ns + setup.write_config(path, new, new) + self.assertEqual(path.stat().st_mtime_ns, before) + + def test_concurrent_change_and_symlink_rejected(self): + path = self.project / ".mcp.json" + path.write_bytes(b"newer") + with self.assertRaisesRegex(ValueError, "changed during"): + setup.write_config(path, b"old", b"replace") + with self.assertRaisesRegex(ValueError, "changed during"): + setup.write_config(path, b"old", b"old") + self.assertEqual(path.read_bytes(), b"newer") + link = self.project / "linked.json" + link.symlink_to(path) + with self.assertRaisesRegex(ValueError, "symlinked"): + setup.read_config(link) + + def test_live_lock_is_not_removed(self): + path = self.project / ".mcp.json" + lock = path.with_name(path.name + ".22b-lock") + lock.touch() + with self.assertRaises(FileExistsError): + setup.write_config(path, None, b"{}") + self.assertTrue(lock.exists()) + + def test_matching_environment_reused_without_pip_install(self): + directory = self.project / "venv" + (directory / "bin").mkdir(parents=True) + (directory / "pyvenv.cfg").touch() + (directory / "bin/python").touch() + result = subprocess.CompletedProcess([], 0, '{"packages_match":true,"wrapper_match":true}') + with patch.object(setup, "run", return_value=result) as run: + setup.install(directory) + self.assertEqual(len(run.call_args_list), 2) + self.assertEqual(run.call_args_list[-1].args[0][-2:], ["pip", "check"]) + + def test_mismatched_wrapper_reinstalls_only_wrapper(self): + directory = self.project / "venv" + (directory / "bin").mkdir(parents=True) + (directory / "pyvenv.cfg").touch() + (directory / "bin/python").touch() + result = subprocess.CompletedProcess([], 0, '{"packages_match":true,"wrapper_match":false}') + with patch.object(setup, "run", return_value=result) as run: + setup.install(directory) + command = run.call_args_list[1].args[0] + self.assertIn("--no-deps", command) + self.assertIn("--force-reinstall", command) + self.assertTrue(str(command[-1]).endswith("mcp-requirements.txt")) + + def test_native_packages_never_fall_back_to_source_builds(self): + directory = self.project / "venv" + (directory / "bin").mkdir(parents=True) + (directory / "pyvenv.cfg").touch() + (directory / "bin/python").touch() + result = subprocess.CompletedProcess([], 0, '{"packages_match":false,"wrapper_match":true}') + with patch.object(setup, "run", return_value=result) as run: + setup.install(directory) + self.assertIn("--only-binary=:all:", run.call_args_list[1].args[0]) + + def test_existing_non_venv_untouched(self): + with self.assertRaisesRegex(ValueError, "not a usable venv"): + setup.install(self.project) + + def test_launcher_uses_absolute_path_and_keeps_venv_symlink(self): + entry = setup.configuration("codex", self.python) + self.assertEqual(entry["command"], str(self.python)) + self.assertEqual(entry["args"], ["-I", str(ROOT / "setup/kepler_server.py")]) + + +if __name__ == "__main__": + unittest.main() diff --git a/tools/README.md b/tools/README.md index c47b33f..f17ae85 100644 --- a/tools/README.md +++ b/tools/README.md @@ -6,6 +6,9 @@ delete caches or upgrade working tools as an incidental part of an experiment. Package references are pinned in [toolchain.json](../toolchain.json). +For direct Kepler tools in Codex or Claude Code, use [agent setup](../setup/README.md). +Package installation and registration with the agent host are separate steps. + | Tool | Installation | Purpose | | --- | --- | --- | | Kepler Formal | [Python-backed MCP + native wheels](kepler-formal/install.md) | SEC verification | diff --git a/tools/kepler-formal/SKILL.md b/tools/kepler-formal/SKILL.md index 6240a32..d1c4950 100644 --- a/tools/kepler-formal/SKILL.md +++ b/tools/kepler-formal/SKILL.md @@ -5,6 +5,14 @@ description: Verify mapped designs in memory or from files with the Python-backe # Verify A Candidate +Prefer the agent's registered Kepler MCP tools for explicit verification. +If unavailable, follow [agent setup](../../setup/README.md); do not claim direct +agent access merely because the Python helper can launch MCP internally. +For live designs, `session.mcp_attachment()` supplies the private descriptor +path and native references for `attach_session` and `verify_session`. +Follow the setup guide's revision and report checks. Keep edits through +`apply_edit`, whose automatic SEC remains mandatory even when direct tools exist. + Use the [package guide](install.md) if needed. Always request SEC, including for combinational edits: the upstream MCP defaults to **LEC**. Keep originals, libraries and constraints unchanged. For iterative Python/Jupyter work use the diff --git a/tools/kepler-formal/install.md b/tools/kepler-formal/install.md index f68eae9..7e92c6b 100644 --- a/tools/kepler-formal/install.md +++ b/tools/kepler-formal/install.md @@ -8,6 +8,10 @@ Use the [shared Python environment](../README.md). Check existing versions and the MCP commit before installing; `kepler-formal-mcp==0.1.0` alone does not distinguish the new Python server from the older CLI wrapper. +For Codex or Claude Code, [agent setup](../../setup/README.md) installs these +pins, checks discovery and safely adds project-scoped MCP configuration. The +generic JSON below is not Codex's configuration format. + ```sh python3 -m venv .venv . .venv/bin/activate diff --git a/tools/live-session.md b/tools/live-session.md index db5b51e..b8b5401 100644 --- a/tools/live-session.md +++ b/tools/live-session.md @@ -41,6 +41,14 @@ Normal sessions and regressions do not need the override. ## Use Across Cells +To let the agent call Kepler directly, first [register MCP with its host](../setup/README.md). +`session.mcp_attachment()` returns a connection-file path, session ID, current +revision and both native design references, without exposing the file's token. +The agent can attach its own MCP server to this same owner and call its tools. +This is additional access, not removal of the helper's automatic post-edit SEC. +Keep direct proofs and edits sequential and confirm the revision after each +proof; the setup guide documents evidence checks and detachment. + Start one fresh Jupyter/Python kernel using that environment and the 22b root as its working directory. Use a local, private connection file; do not expose the kernel or its credentials to a network or include them in artifacts. diff --git a/tools/live_session.py b/tools/live_session.py index e7a5f24..7d0c2d7 100644 --- a/tools/live_session.py +++ b/tools/live_session.py @@ -252,6 +252,17 @@ def status(self): self._check() return self._record() + def mcp_attachment(self): + """Return local attachment coordinates for an agent's independent MCP client. + + The private descriptor stays on disk; its token is never returned. This + does not transfer ownership or replace automatic post-edit verification. + """ + with self._inspection_access(): + return {"connection_file": str(self._bridge.connection_file), + "session_id": self._session_id, "revision": self.revision, + "design1": dict(self._golden_ref), "design2": dict(self._candidate_ref)} + @contextmanager def _inspection_access(self): if not self._operation.acquire(blocking=False):