diff --git a/.github/workflows/gcd-reference-verify.yml b/.github/workflows/gcd-reference-verify.yml index a34018a..68dbe64 100644 --- a/.github/workflows/gcd-reference-verify.yml +++ b/.github/workflows/gcd-reference-verify.yml @@ -6,6 +6,8 @@ on: paths: - '.github/workflows/gcd-reference-verify.yml' - 'scripts/gcd_reference_regression.py' + - 'scripts/live_inspection_regression.py' + - 'scripts/live_session_regression.py' - 'examples/backend/gcd/**' - 'toolchain.json' - 'tools/**' @@ -14,6 +16,8 @@ on: paths: - '.github/workflows/gcd-reference-verify.yml' - 'scripts/gcd_reference_regression.py' + - 'scripts/live_inspection_regression.py' + - 'scripts/live_session_regression.py' - 'examples/backend/gcd/**' - 'toolchain.json' - 'tools/**' @@ -71,6 +75,8 @@ jobs: python scripts/gcd_reference_regression.py --work-dir "$RUN" --stage prepare - name: Baseline OpenROAD physical design flow run: python scripts/gcd_reference_regression.py --work-dir "$RUN" --stage baseline + - name: Live candidate inspection checkpoints through Naja-Scope MCP + run: python scripts/live_inspection_regression.py --work-dir runs/live-inspection - name: Naja-Scope MCP connectivity inspection run: python scripts/gcd_reference_regression.py --work-dir "$RUN" --stage inspect - name: Apply the reviewed reference edit with NajaEDA @@ -88,6 +94,7 @@ jobs: name: gcd-packaged-reference path: | runs/gcd-reference/ + runs/live-inspection/ .cache/gcd-tools/*.json .cache/gcd-tools/*.txt .cache/gcd-tools/*.log diff --git a/SKILL.md b/SKILL.md index 3416498..9234ad5 100644 --- a/SKILL.md +++ b/SKILL.md @@ -29,12 +29,16 @@ or comparison afterward, not hints for independent discovery. stale output files as evidence for a new run. 3. Inspect using reports and, when structural connectivity matters, [Naja-Scope](tools/naja-scope/SKILL.md). Separate observations from hypotheses. + In a live editing session, refresh Scope only when the next decision needs + current connectivity; use its revision-labelled inspection checkpoint, not + a stale copy left from an earlier edit. 4. Use [NajaEDA](tools/najaeda/SKILL.md) for structural edits. Review and syntax check generated code before running it with only the needed file access. 5. Run [Kepler Formal SEC through MCP](tools/kepler-formal/SKILL.md). For iterative in-memory work, use the [persistent session](tools/live-session.md): keep one unchanged golden and one cumulatively edited candidate, with automatic SEC - after every edit and no intermediate design dumps. If a design is later + after every edit and no design dumps for verification. Optional inspection + copies never replace either live design. If a design is later exported for another tool, verify that exported representation separately. Preserve the structured outcome, logs and actual output coverage. 6. For backend tasks, rerun [OpenROAD](tools/openroad/SKILL.md) with the same diff --git a/flow/backend/SKILL.md b/flow/backend/SKILL.md index 329a4fc..e891ec3 100644 --- a/flow/backend/SKILL.md +++ b/flow/backend/SKILL.md @@ -14,6 +14,9 @@ LEF/technology data and an SDC; RTL synthesis is not implicit in this flow. slew, capacitance and fanout. Check that constraints and units are meaningful. 3. Use [Naja-Scope](../../tools/naja-scope/SKILL.md) to establish the target cone and all boundary consumers. A timing path is not the complete connectivity. + Reuse a current inspection copy across queries. After an edit, refresh only + when a new decision needs candidate connectivity, including a changed critical + path after rerouting. Keep baseline evidence labelled as baseline. 4. Propose a specific Boolean or architectural transformation, with expected benefit and area/power/hold risks. Do not describe cell sizing as logic restructuring. If the rewrite is already specified, skip new model analysis. diff --git a/scripts/live_inspection_regression.py b/scripts/live_inspection_regression.py new file mode 100644 index 0000000..355ceb0 --- /dev/null +++ b/scripts/live_inspection_regression.py @@ -0,0 +1,94 @@ +"""Real file-based Scope checkpoints alongside cumulative live NajaEDA/SEC edits.""" + +import argparse +import asyncio +from pathlib import Path +import sys + + +ROOT = Path(__file__).resolve().parents[1] +sys.path.insert(0, str(ROOT)) + +from scripts.gcd_reference_regression import clean_env, save, scope_payload +from scripts.live_session_regression import LIBERTY, FIRST, SECOND +from tools.live_session import LiveDesignSession + + +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) + params = StdioServerParameters(command=sys.executable, args=["-m", "naja_scope.server"], + env=clean_env(), cwd=str(ROOT)) + with LiveDesignSession(source, [library], work / "session") as live: + assert live.verify()["status"] == "proved" + initial = live.status() + with (work / "scope-server.log").open("w") as log: + async with stdio_client(params, errlog=log) as streams: + async with ClientSession(*streams) as scope: + await scope.initialize() + calls = [] + + async def call(name, arguments=None): + response = await scope.call_tool(name, arguments or {}) + value = scope_payload(response) + calls.append({"tool": name, "arguments": arguments or {}, "result": value}) + save(work / "scope-calls.json", calls) + return value + + async def load(artifact): + assert live.inspection_status(artifact["manifest"])["current"] + await call("reset_universe") # Only the separate Scope server. + await call("load_liberty", {"files": artifact["liberty_files"]}) + await call("load_verilog", {"files": [artifact["verilog_file"]]}) + loaded = await call("status") + assert loaded["loaded"] and loaded["top"]["name"] == artifact["top"] + assert artifact["verilog_file"] in loaded["loaded_files"] + + async def names(): + result = await call("get_hierarchy", {"depth": 1, "limit": 20}) + assert not result["root"].get("has_more") + return {child["name"] for child in result["root"]["children"]} + + old = live.export_inspection() + await load(old) + assert await names() == {"g"} + for script, expected in ((FIRST, {"g", "h"}), (SECOND, {"g", "h1", "h2"})): + before_names = await names() + proof = live.apply_edit(script) + assert proof["status"] == "proved" and proof["proved_outputs"] == 1 + assert not live.inspection_status(old["manifest"])["current"] + # No automatic reset/reload: the old server copy really stays old. + assert await names() == before_names + before = live.status() + fresh = live.export_inspection() + assert live.status() == before + assert fresh["export_equivalence"] == "not_checked" + await load(fresh) + assert await names() == expected + assert await names() == expected # Reuse without another load. + assert live.inspection_status(fresh["manifest"])["current"] + assert live.status()["golden_sha256"] == initial["golden_sha256"] + assert live.status()["candidate_reference"] == initial["candidate_reference"] + old = fresh + print(f"PASS: live SEC and separate Scope refresh for revision {proof['revision']}", + flush=True) + assert len(list((work / "session/inspections").glob("*/manifest.json"))) == 3 + save(work / "result.json", { + "status": "passed", "candidate_revisions": 2, + "scope_loads": 3, "stale_copy_detected": True, + "fresh_queries_reused": True, "golden_preserved": True, + "live_sec_proved_outputs": 1, "live_sec_total_outputs": 1, + "export_equivalence": "not_checked", + }) + + +if __name__ == "__main__": + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--work-dir", type=Path, required=True) + args = parser.parse_args() + asyncio.run(asyncio.wait_for(run(args.work_dir.resolve()), timeout=180)) diff --git a/tests/test_live_session.py b/tests/test_live_session.py index 3111b2f..5fdbce7 100644 --- a/tests/test_live_session.py +++ b/tests/test_live_session.py @@ -1,5 +1,6 @@ """Offline session-policy tests; real kernel/SEC checks are a separate runner.""" +import hashlib import json import os from pathlib import Path @@ -64,7 +65,7 @@ def setUp(self): temp = tempfile.TemporaryDirectory() self.addCleanup(temp.cleanup) session = live.LiveDesignSession.__new__(live.LiveDesignSession) - session.directory = Path(temp.name) + session.directory = Path(temp.name).resolve() session.timeout, session.revision, session._attempt = 5, 0, 0 session._pending = session._closed = False session.state, session.proof = "unverified", None @@ -73,6 +74,9 @@ def setUp(self): session._naja = SimpleNamespace(NLUniverse=SimpleNamespace(get=lambda: session._universe)) session._golden = SimpleNamespace(signature="golden") session._candidate = SimpleNamespace(signature="candidate") + session._candidate.getName = lambda: "fixture" + session._candidate.dumpVerilog = Mock(side_effect=lambda directory, name: + (Path(directory) / name).write_text("module fixture(); endmodule\n")) session._golden_hash, session._candidate_hash = "golden", "candidate" session._golden_ref, session._candidate_ref = dict(GOLDEN_REF), dict(CANDIDATE_REF) session._netlist = SimpleNamespace(get_top=lambda: session._candidate) @@ -81,6 +85,11 @@ def setUp(self): session._client = Mock() session._client.busy.return_value = False session._client.call.return_value = attached_result() + library = session.directory / "source.lib" + library.write_text("library(cells) {}\n") + session._liberty_paths = [library] + session._source_hashes = {str(library): hashlib.sha256(library.read_bytes()).hexdigest()} + session._inspections = {} self.session = session fingerprint = patch.object(live, "_fingerprint", side_effect=lambda design: design.signature) fingerprint.start() @@ -236,6 +245,130 @@ def test_invalid_native_handle_clears_previous_proof(self): self.assertEqual(self.session.state, "invalid") self.assertIsNone(self.session.proof) + def test_inspection_is_explicit_read_only_and_not_an_export_proof(self): + self.session.verify() + before = self.session.status() + calls = self.session._client.call.call_count + artifact = self.session.export_inspection() + self.assertEqual(self.session.status(), before) + self.assertEqual(self.session._client.call.call_count, calls) + self.assertEqual(artifact["revision"], 0) + self.assertEqual(artifact["candidate_reference"], CANDIDATE_REF) + self.assertEqual(artifact["export_equivalence"], "not_checked") + self.assertTrue(self.session.inspection_status(artifact["manifest"])["current"]) + for name, digest in artifact["file_sha256"].items(): + self.assertEqual(hashlib.sha256(Path(name).read_bytes()).hexdigest(), digest) + self.assertEqual(Path(name).stat().st_mode & 0o222, 0) + self.assertEqual(Path(artifact["liberty_files"][0]).read_bytes(), + self.session._liberty_paths[0].read_bytes()) + self.session._universe.setTopDesign.assert_not_called() + self.session._universe.destroy.assert_not_called() + + def test_inspections_are_unique_and_status_does_not_export(self): + first = self.session.export_inspection() + second = self.session.export_inspection() + self.assertNotEqual(first["manifest"], second["manifest"]) + for artifact in (first, second): + self.assertTrue(self.session.inspection_status(artifact["manifest"])["current"]) + self.assertEqual(self.session._candidate.dumpVerilog.call_count, 2) + + def test_edit_marks_old_inspection_stale_without_automatic_export(self): + artifact = self.session.export_inspection() + self.session.apply_edit("def edit(top):\n pass") + result = self.session.inspection_status(artifact["manifest"]) + self.assertFalse(result["current"]) + self.assertEqual(result["reasons"], ["candidate_revision_changed"]) + self.assertEqual(result["current_revision"], 1) + self.assertEqual(self.session._candidate.dumpVerilog.call_count, 1) + fresh = self.session.export_inspection() + self.assertTrue(self.session.inspection_status(fresh["manifest"])["current"]) + + def test_inspection_returned_metadata_cannot_change_retained_record(self): + artifact = self.session.export_inspection() + manifest = artifact["manifest"] + artifact["revision"] = 999 + artifact["candidate_reference"]["db_id"] = 44 + artifact["file_sha256"].clear() + self.assertTrue(self.session.inspection_status(manifest)["current"]) + self.assertEqual(self.session.inspection_status(manifest)["revision"], 0) + + def test_modified_or_missing_inspection_files_never_report_current(self): + for field in ("manifest", "verilog_file", "liberty_files"): + artifact = self.session.export_inspection() + path = Path(artifact[field][0] if field == "liberty_files" else artifact[field]) + path.chmod(0o600) + path.write_text("{}") + self.assertFalse(self.session.inspection_status(artifact["manifest"])["current"]) + path.unlink() + self.assertFalse(self.session.inspection_status(artifact["manifest"])["current"]) + + def test_other_session_manifests_rejected(self): + with self.assertRaisesRegex(ValueError, "not exported"): + self.session.inspection_status(self.session.directory / "unknown.json") + + def test_changed_source_liberty_refuses_new_export_but_old_copy_stays_valid(self): + artifact = self.session.export_inspection() + self.session._liberty_paths[0].write_text("changed") + with self.assertRaisesRegex(RuntimeError, "Liberty source changed"): + self.session.export_inspection() + self.assertEqual(len(self.session._inspections), 1) + self.assertTrue(self.session.inspection_status(artifact["manifest"])["current"]) + + def test_export_error_does_not_invalidate_live_proof_or_publish_manifest(self): + self.session.verify() + before = self.session.status() + self.session._candidate.dumpVerilog.side_effect = OSError("disk full") + with self.assertRaisesRegex(OSError, "disk full"): + self.session.export_inspection() + self.assertEqual(self.session.status(), before) + self.assertFalse(self.session._inspections) + self.assertTrue(list(self.session.directory.glob("inspections/*/error.json"))) + + def test_empty_export_is_rejected(self): + self.session._candidate.dumpVerilog.side_effect = None + with self.assertRaisesRegex(RuntimeError, "no Verilog"): + self.session.export_inspection() + self.assertFalse(self.session._inspections) + + def test_export_detects_unexpected_live_mutation(self): + def corrupt(directory, name): + (Path(directory) / name).write_text("module fixture(); endmodule") + self.session._candidate.signature = "corrupted" + self.session._candidate.dumpVerilog.side_effect = corrupt + with self.assertRaises(RuntimeError): + self.session.export_inspection() + self.assertEqual(self.session.state, "invalid") + self.assertFalse(self.session._inspections) + + def test_busy_and_pending_verification_block_inspection(self): + self.session._operation.acquire() + try: + with self.assertRaisesRegex(RuntimeError, "Another session operation"): + self.session.export_inspection() + finally: + self.session._operation.release() + self.session._client.busy.return_value = True + with self.assertRaisesRegex(RuntimeError, "still running"): + self.session.export_inspection() + self.session._client.busy.return_value = False + self.session._pending = True + with self.assertRaisesRegex(RuntimeError, "unresolved"): + self.session.export_inspection() + self.session._candidate.dumpVerilog.assert_not_called() + + def test_closed_session_cannot_export(self): + self.session.close() + with self.assertRaisesRegex(RuntimeError, "closed"): + self.session.export_inspection() + + def test_unproven_and_rejected_candidates_are_inspectable_without_promotion(self): + for state in ("unproven", "rejected", "edit_error"): + self.session.state = state + artifact = self.session.export_inspection() + self.assertEqual(artifact["live_state"], state) + self.assertEqual(self.session.state, state) + self.assertIsNone(self.session.proof) + if __name__ == "__main__": unittest.main() diff --git a/tools/live-session.md b/tools/live-session.md index 15a03d9..db5b51e 100644 --- a/tools/live-session.md +++ b/tools/live-session.md @@ -5,6 +5,9 @@ One dedicated kernel holds two designs: immutable golden and mutable candidate. The candidate is never replaced by a reload between iterations. Both designs have their own database and loaded Liberty definitions; library sharing and Naja-Scope attachment are deferred. No design dump is needed for verification. +For on-demand inspection with the existing file-based Scope server, use +[inspection checkpoints](naja-scope/checkpoints.md). They export a labelled copy +without replacing either live design. ## Setup @@ -97,6 +100,13 @@ Inspect `session.status()` for current revision, state and proof. Closing with `session.close()` detaches the MCP and destroys only this session's universe. Opening refuses an already-loaded universe rather than resetting user data. +`session.export_inspection()` explicitly exports the current candidate for a +separate Scope server and returns its manifest and loading paths. +`session.inspection_status(manifest_path)` checks that copy's revision and +file integrity without exporting again. Neither method runs SEC, certifies the +exported representation, or changes the live proof. Ordinary edit/verify calls +still perform no exports. Inspection of a rejected candidate is diagnostic only. + ## Outcomes And Recovery | State | Meaning | diff --git a/tools/live_session.py b/tools/live_session.py index b33a659..e7a5f24 100644 --- a/tools/live_session.py +++ b/tools/live_session.py @@ -2,6 +2,7 @@ import asyncio from concurrent.futures import Future +from contextlib import contextmanager import hashlib import importlib.util import json @@ -9,6 +10,7 @@ from pathlib import Path import queue import sys +import tempfile import threading from tools.edit_validation import editing_function @@ -126,7 +128,8 @@ class LiveDesignSession: Use only in a dedicated trusted Python/Jupyter kernel. The editing contract is deliberately restricted; neither Python nor the Naja native API is an OS - sandbox. No design is exported, reloaded or reset between iterations. + sandbox. Verification needs no exports or reloads. Inspection copies are + exported only on an explicit call, never reloaded into this kernel. """ def __init__(self, reference, liberty_files, work_dir, *, timeout=600, @@ -151,12 +154,15 @@ def __init__(self, reference, liberty_files, work_dir, *, timeout=600, self._bridge = self._client = self._universe = None self._databases = [] self._attempt = 0 + self._inspections = {} try: identity = SEC.package_identity(development_mcp_checkout) SEC.save(self.directory / "packages.json", identity) paths = [Path(reference).resolve(strict=True), *[Path(p).resolve(strict=True) for p in liberty_files]] - SEC.save(self.directory / "source-hashes.json", { - str(path): hashlib.sha256(path.read_bytes()).hexdigest() for path in paths}) + self._liberty_paths = paths[1:] + self._source_hashes = { + str(path): hashlib.sha256(path.read_bytes()).hexdigest() for path in paths} + SEC.save(self.directory / "source-hashes.json", self._source_hashes) self._universe = naja.NLUniverse.create() designs = [] for _ in range(2): @@ -246,6 +252,102 @@ def status(self): self._check() return self._record() + @contextmanager + def _inspection_access(self): + if not self._operation.acquire(blocking=False): + raise RuntimeError("Another session operation is running") + try: + self._check() + if self._pending: + raise RuntimeError("A timed-out proof is unresolved; verify again when idle before inspection") + if not self._bridge.lock.acquire(blocking=False): + raise RuntimeError("Native work is still running; inspection is blocked") + try: + self._check() + try: + yield + finally: + self._check() + finally: + self._bridge.lock.release() + finally: + self._operation.release() + + def export_inspection(self): + """Export a fresh candidate copy for a separate, file-based Scope server. + + The manifest describes an inspection artifact, not a proof of its + exported representation. This method does not load or reset any design. + """ + with self._inspection_access(): + root = self.directory / "inspections" + root.mkdir(exist_ok=True) + directory = Path(tempfile.mkdtemp(prefix=f"revision-{self.revision:04}-", dir=root)) + manifest = directory / "manifest.json" + libraries = [] + hashes = {} + try: + for index, source in enumerate(self._liberty_paths): + data = source.read_bytes() + digest = hashlib.sha256(data).hexdigest() + if digest != self._source_hashes[str(source)]: + raise RuntimeError("Liberty source changed since the live session was loaded") + target = directory / f"cells-{index:03}.lib" + target.write_bytes(data) + libraries.append(str(target)) + hashes[str(target)] = digest + verilog = directory / "candidate.v" + self._candidate.dumpVerilog(str(directory), verilog.name) + if not verilog.is_file() or not verilog.stat().st_size: + raise RuntimeError("Inspection export produced no Verilog") + hashes[str(verilog)] = hashlib.sha256(verilog.read_bytes()).hexdigest() + self._check() + record = { + "schema": "22b-inspection-v1", "purpose": "inspection-only", + "manifest": str(manifest), "revision": self.revision, + "candidate_reference": dict(self._candidate_ref), + "candidate_sha256": self._candidate_hash, + "top": self._candidate.getName(), "live_state": self.state, + "export_equivalence": "not_checked", + "verilog_file": str(verilog), "liberty_files": libraries, + "file_sha256": hashes, + } + SEC.save(manifest, record) + for path in [manifest, *map(Path, hashes)]: + path.chmod(0o400) + self._inspections[str(manifest)] = record + return json.loads(json.dumps(record)) + except BaseException as error: + # Keep failed exports for diagnosis, but never register them as usable. + SEC.save(directory / "error.json", {"error": str(error)}) + raise + + def inspection_status(self, manifest): + """Check an exported copy's provenance and freshness, not Scope's server state.""" + with self._inspection_access(): + key = str(Path(manifest).resolve()) + if key not in self._inspections: + raise ValueError("Inspection manifest was not exported by this live session") + record = self._inspections[key] + reasons = [] + if (record["revision"] != self.revision + or record["candidate_sha256"] != self._candidate_hash): + reasons.append("candidate_revision_changed") + try: + if json.loads(Path(key).read_text()) != record: + reasons.append("manifest_modified") + except (OSError, ValueError): + reasons.append("manifest_missing_or_unreadable") + for name, digest in record["file_sha256"].items(): + try: + if hashlib.sha256(Path(name).read_bytes()).hexdigest() != digest: + reasons.append("inspection_file_modified: " + name) + except OSError: + reasons.append("inspection_file_missing_or_unreadable: " + name) + return {"manifest": key, "revision": record["revision"], + "current_revision": self.revision, "current": not reasons, + "reasons": reasons, "export_equivalence": "not_checked"} + def apply_edit(self, script): function = editing_function(script) if not self._operation.acquire(blocking=False): diff --git a/tools/naja-scope/SKILL.md b/tools/naja-scope/SKILL.md index fdcd6d0..faf42ad 100644 --- a/tools/naja-scope/SKILL.md +++ b/tools/naja-scope/SKILL.md @@ -9,6 +9,14 @@ Use the [package guide](install.md). Discover the installed typed-tool schemas, then load Liberty and Verilog with `load_liberty` and `load_verilog`. Confirm the top and loaded design with `status` before querying. +The pinned MCP server owns a separate loaded copy, not the live editing +candidate. Load original files once for baseline analysis. For a persistent +NajaEDA session, use [inspection checkpoints](checkpoints.md): export on demand, +record which revision Scope loaded, and check freshness before using its answers +for a current-candidate decision. Reuse current copies; do not dump after every +edit or reload before every query. Refresh when the next decision needs changed +connectivity, not merely because an edit occurred. + - Use `resolve` for exact hierarchical objects; retain underscores and bit indices. - Use `get_drivers` to identify boundary input sources. - Use `get_loads` on **every** output of the proposed replacement group. Include diff --git a/tools/naja-scope/checkpoints.md b/tools/naja-scope/checkpoints.md new file mode 100644 index 0000000..68a76e3 --- /dev/null +++ b/tools/naja-scope/checkpoints.md @@ -0,0 +1,90 @@ +# Inspect A Live Candidate Without Binding + +Use this file-based handoff with the pinned Naja-Scope MCP server. Golden, +candidate and automatic SEC remain in their existing Python/Jupyter kernel. +Do not import Scope or call its load/reset tools inside that kernel. + +## Decide Whether To Refresh + +- For original-design questions, use the baseline files and retain baseline-labelled evidence. +- For current drivers, fanout, replacement boundaries or a newly reported timing + path, check whether Scope's loaded copy matches the live candidate revision. +- Reuse the same loaded copy for multiple queries while current. An edit makes + it historical, but does not require a refresh until current inspection is needed. +- Inspection is also useful for diagnosing a rejected or partially executed + edit. It does not turn that candidate into an accepted or proven design. + +## Export And Load + +In the existing editing kernel, outside the generated `edit(top)` script: + +```python +inspection = session.export_inspection() +manifest = inspection["manifest"] +assert session.inspection_status(manifest)["current"] +``` + +This creates a fresh private directory under the session's `inspections/`, with +read-only `candidate.v`, copies of the original Liberty files and a manifest. +It records the native candidate reference, revision, top and file hashes. +It holds the shared native lock, checks the live designs before/after export, +and does not reset/reload a design or advance the edit revision. A changed +Liberty source or failed dump is an error, not a usable checkpoint. + +In the **separate Naja-Scope MCP server**, using its discovered schemas: + +1. For a refresh, call `reset_universe` there only. This clears that server's + old copy, never the editing kernel. A new empty server needs no reset. +2. Call `load_liberty` with `files=inspection["liberty_files"]` (skip if empty). +3. Call `load_verilog` with `files=[inspection["verilog_file"]]`, retaining + strict unresolved-cell checking. +4. Confirm the returned top and `status` loaded files match the manifest, then + record that manifest as the copy loaded by this Scope server. If any loading + step fails, do not reuse the previous loaded-copy claim. +5. Use the typed inspection tools. Save query arguments and responses together + with the manifest path and revision. + +The paths must be accessible to the Scope server on the same host/filesystem. +The helper does not launch Scope, call its tools or monitor what another client +loads. Track the loaded manifest per server; use separate servers for concurrent +baseline/candidate inspection, or explicitly reset and switch one server. + +## Check Freshness + +In the editing kernel, before using Scope evidence for the current candidate: + +```python +freshness = session.inspection_status(manifest) +if not freshness["current"]: + print(freshness["reasons"]) + # Export and load a fresh copy only if current-candidate inspection is needed. +``` + +This checks the retained export record, current revision and artifact hashes. +It rejects manifests from other live sessions. It never silently refreshes. +Check again after a group of queries if editing could have occurred in between; +historical results remain historical even after loading a newer copy. +Do not edit read-only inspection files; make a new export instead. Read-only +permissions and hashes detect accidents, not hostile same-user Python code. + +Freshness means the copy came from the current revision and its files are +unchanged, **not** that export preserved connectivity. Every manifest says +`export_equivalence: not_checked`. In-memory SEC is not a proof of dumped +Verilog; if an inspection answer will drive a subsequent edit, confirm its +target objects and connections in the live candidate before editing. Exported +Verilog used for physical measurements or equivalence claims must pass the +separate [file-based SEC](../kepler-formal/SKILL.md) handoff. Inspection never +replaces automatic SEC after a live edit. + +## Validate The Handoff + +With the pinned packages installed, run: + +```sh +python scripts/live_inspection_regression.py --work-dir runs/inspection-check +``` + +This uses real NajaEDA, Kepler SEC and a separate Naja-Scope MCP server. It checks +two cumulative edits, stale-copy detection, explicit refresh, repeated queries +without reloading, and unchanged golden/proof state across export. Run +`scripts/live_session_regression.py` separately for the Jupyter no-export flow.