Add direct agent MCP setup and live attachment regression

.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

.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-*

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.

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

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()))

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).

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)