Add revision-aware Naja-Scope inspection checkpoints

.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

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

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.

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

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

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 |