diff --git a/.github/workflows/flow-modes-verify.yml b/.github/workflows/flow-modes-verify.yml new file mode 100644 index 0000000..2076208 --- /dev/null +++ b/.github/workflows/flow-modes-verify.yml @@ -0,0 +1,62 @@ +name: Managed and direct flow modes + +on: + workflow_dispatch: + push: + paths: + - '.github/workflows/flow-modes-verify.yml' + - 'SKILL.md' + - 'flow/**' + - 'tools/**' + - 'scripts/**' + - 'tests/**' + - 'setup/**' + - 'toolchain.json' + pull_request: + paths: + - '.github/workflows/flow-modes-verify.yml' + - 'SKILL.md' + - 'flow/**' + - 'tools/**' + - 'scripts/**' + - 'tests/**' + - 'setup/**' + - 'toolchain.json' + +permissions: + contents: read + +jobs: + tool-modes: + runs-on: ubuntu-24.04 + timeout-minutes: 20 + env: + PYTHONPATH: '' + NAJAEDA_SRC: '' + steps: + - uses: actions/checkout@v4 + - uses: actions/setup-python@v5 + with: + python-version: '3.13' + - name: Offline skills, mode routing and proof guards + run: python -m unittest discover -s tests -v + - name: Install or reuse packaged tools and check MCP discovery + run: | + mkdir -p .cache/mode-agent + python setup/mcp.py configure --client codex --project .cache/mode-agent \ + --venv .cache/mode-python --apply + .cache/mode-python/bin/python setup/mcp.py check --venv .cache/mode-python + - name: Managed history inside a real Jupyter kernel + run: .cache/mode-python/bin/python scripts/versioned_session_regression.py --jupyter --work-dir runs/mode-managed + - name: Direct NajaEDA and MCP tools without the flow helper + run: .cache/mode-python/bin/python scripts/direct_tools_regression.py --work-dir runs/mode-direct + - name: Preserve actual mode evidence + if: always() + uses: actions/upload-artifact@v4 + with: + name: flow-mode-regressions + path: | + runs/mode-managed/ + runs/mode-direct/ + if-no-files-found: warn + retention-days: 14 diff --git a/.github/workflows/gcd-undo-verify.yml b/.github/workflows/gcd-undo-verify.yml new file mode 100644 index 0000000..c1ec068 --- /dev/null +++ b/.github/workflows/gcd-undo-verify.yml @@ -0,0 +1,98 @@ +name: GCD packaged undo + +on: + workflow_dispatch: + push: + paths: + - '.github/workflows/gcd-undo-verify.yml' + - 'scripts/**' + - 'setup/**' + - 'examples/backend/gcd/**' + - 'toolchain.json' + - 'tools/**' + - 'tests/**' + pull_request: + paths: + - '.github/workflows/gcd-undo-verify.yml' + - 'scripts/**' + - 'setup/**' + - 'examples/backend/gcd/**' + - 'toolchain.json' + - 'tools/**' + - 'tests/**' + +permissions: + contents: read + +jobs: + undo-replay: + runs-on: ubuntu-24.04 + timeout-minutes: 45 + defaults: + run: + shell: bash + env: + RUN: runs/gcd-undo + PYTHONPATH: '' + NAJAEDA_SRC: '' + steps: + - uses: actions/checkout@v4 + - uses: actions/setup-python@v5 + with: + python-version: '3.13' + - name: Offline checks + run: python -m unittest discover -s tests -v + - name: Install Nix (reuse an existing installation) + uses: cachix/install-nix-action@v31 + with: + install_url: https://releases.nixos.org/nix/nix-2.35.1/install + enable_kvm: false + extra_nix_config: | + experimental-features = nix-command flakes + max-jobs = 0 + builders = + - name: Obtain cached OpenROAD (fail before downloading dependencies on a cache miss) + run: | + mkdir -p .cache/gcd-tools + df -h . /nix | tee .cache/gcd-tools/disk-before.txt + openroad=$(python -c 'import json; print(json.load(open("toolchain.json"))["openroad"]["installable"])') + cache=$(python -c 'import json; print(json.load(open("toolchain.json"))["openroad"]["cache"])') + bash tools/install-cached-package.sh openroad "$openroad" "$cache" .cache/gcd-tools + echo "$PWD/.cache/gcd-tools/openroad/bin" >> "$GITHUB_PATH" + - name: Install native Python wheels and pinned pure-Python Kepler MCP package + run: | + 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 existing live-session regressions + 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 + python scripts/live_inspection_regression.py --work-dir runs/live-inspection + - name: Version history retention, failures, undo and continued editing + run: python scripts/versioned_session_regression.py --jupyter --work-dir runs/versioned-session + - name: GCD baseline, edit and undo with Scope, SEC and three fresh OpenROAD runs + run: | + openroad -version | tee .cache/gcd-tools/openroad-version.txt + python scripts/gcd_undo_regression.py --work-dir "$RUN" + - name: Preserve baseline, edited and restored observations and reports + if: always() + uses: actions/upload-artifact@v4 + with: + name: gcd-packaged-undo + path: | + runs/gcd-undo/ + runs/versioned-session/ + runs/live-inspection/ + runs/agent-mcp/ + runs/live-session/ + .cache/gcd-tools/*.json + .cache/gcd-tools/*.txt + .cache/gcd-tools/*.log + if-no-files-found: warn + retention-days: 14 diff --git a/AGENTS.md b/AGENTS.md index 20336fc..fbe11b7 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -1,6 +1,7 @@ # Working In 22b -- Read [SKILL.md](SKILL.md), then the selected flow skill. Load tool references +- Read [SKILL.md](SKILL.md), then the selected flow and execution-mode skills. + Honor direct mode without importing the flow helper. Load tool references only when their operation is needed. - Keep reusable tool knowledge in `tools/`, application guidance in `flow/`, and design-specific inputs and recipes in the matching `examples/` directory. diff --git a/README.md b/README.md index dc31fcb..e8779ab 100644 --- a/README.md +++ b/README.md @@ -8,8 +8,8 @@ measurement. There is no chatbot runtime or model dependency in this repository. ```text SKILL.md Parent orchestration skill -flow/backend/ Physical-design analysis and improvement -flow/rtl/ RTL authoring and design changes +flow/backend/ Backend guidance, managed/ and direct/ skills +flow/rtl/ RTL guidance, managed/ and direct/ skills examples/backend/gcd/ GCD design and independent model task examples/rtl/ RTL example conventions tools/ Shared tool skills and package installation guides @@ -36,17 +36,33 @@ if the inline player is unavailable. 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. +2. Choose the [backend](flow/backend/SKILL.md) or [RTL](flow/rtl/SKILL.md) flow, + then its managed or direct execution flavor. 3. For a concrete backend attempt, give the model the [GCD task](examples/backend/gcd/task.md). An agent can read these files directly. [AGENTS.md](AGENTS.md) points agents to the same entry point; human users can follow the same procedures. Skills are -instructions, not a security sandbox. For iterative work, the optional -[persistent Python/Jupyter session](tools/live-session.md) validates each edit -and automatically runs SEC on the cumulative candidate against unchanged -golden, without design dumps or reloads between edits. The model stays in the -same kernel throughout. The pinned MCP includes its attached-session report API; -the existing file-based flow is unchanged. +instructions, not a security sandbox. Both flows offer two flavors: + +| Flow | Helper-managed | Direct tools, no flow helper | +| --- | --- | --- | +| Backend | [Managed skill](flow/backend/managed/SKILL.md) | [Direct skill](flow/backend/direct/SKILL.md) | +| RTL | [Managed skill](flow/rtl/managed/SKILL.md) | [Direct skill](flow/rtl/direct/SKILL.md) | + +Honor the requested flavor; managed is the default for iterative structural +work. Both share [session policies](flow/session-policy.md) and tool documentation. +Direct mode follows an explicit [file-based recipe](flow/direct-revisions.md), +with NajaEDA Python and direct Scope/Kepler MCP calls. Required checks are agent +responsibilities, not automatically enforced by instructions. Neither mode adds +an RTL elaboration frontend or changes tool input support. + +Managed mode starts the [versioned Python/Jupyter session](tools/live-session.md). +It validates each edit, +runs SEC against unchanged golden and separately verifies numbered Verilog +checkpoints. It keeps ten recent edits plus baseline by default, supports undo, +and can retain a measured best result independently. The model stays in the same +kernel; only undo reloads the candidate. The original no-export helper and +existing file-based flow remain available without changing existing callers. ## Verification And Evidence @@ -70,3 +86,6 @@ The separate [GCD reference workflow](.github/workflows/gcd-reference-verify.yml tests package installation and real tool stages using the saved solution under [reference/](examples/backend/gcd/reference/README.md). It uses no model, and its success does not establish that a model can solve the independent task. +The [mode regression](.github/workflows/flow-modes-verify.yml) checks both skill +routes, real managed history and helper-free direct tool execution. It tests +structural fixtures, not a model's ability to follow skills or synthesize RTL. diff --git a/SKILL.md b/SKILL.md index 3ccf141..1561b25 100644 --- a/SKILL.md +++ b/SKILL.md @@ -9,6 +9,10 @@ description: Coordinate open-source hardware design tools for backend optimizati - For a mapped design and physical reports, read [backend](flow/backend/SKILL.md). - For RTL creation or changes, read [RTL](flow/rtl/SKILL.md). +- Select that flow's **managed** or **direct** skill before editing. Honor an + explicitly requested mode; otherwise use managed for iterative structural + work. Read only the selected mode, not both. Switching requires a deliberate + handoff of inputs and evidence, not a silent fallback after a failure. - 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 @@ -32,18 +36,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. + Refresh Scope when the next decision needs a different numbered revision; + do not reuse a stale or historical copy for a current-design question. 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 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. +5. Run [Kepler Formal SEC through MCP](tools/kepler-formal/SKILL.md) and retain + actual outcomes and coverage. Managed mode enforces live SEC and separately + checks exported checkpoints through its helper. Direct mode calls the tools + explicitly; the skills require the checks but do not mechanically enforce + them. Follow the shared [session policy](flow/session-policy.md). Never + describe a live proof as proof of an exported file. 6. For backend tasks, rerun [OpenROAD](tools/openroad/SKILL.md) with the same physical setup. Compare timing, area, estimated power, hold and routing checks. diff --git a/flow/backend/SKILL.md b/flow/backend/SKILL.md index e891ec3..bda4ed8 100644 --- a/flow/backend/SKILL.md +++ b/flow/backend/SKILL.md @@ -5,6 +5,17 @@ description: Improve a synthesized design using OpenROAD physical reports, Naja- # Backend Improvement +Select one execution flavor: + +- [Managed](managed/SKILL.md): the Python session helper handles edits, SEC, + checkpoints and undo. Default for iterative structural work. +- [Direct](direct/SKILL.md): the agent coordinates tools and files without the + flow helper. Use when explicitly requested; do not silently switch to managed. + +Both follow the [session policy](../session-policy.md). Measurements belong to +an exact numbered revision and unchanged physical setup, not just "the latest" +filename. Scope must inspect the restored revision after undo. + Read the [parent contract](../../SKILL.md). Start from mapped Verilog, Liberty, LEF/technology data and an SDC; RTL synthesis is not implicit in this flow. diff --git a/flow/backend/direct/SKILL.md b/flow/backend/direct/SKILL.md new file mode 100644 index 0000000..9173ee3 --- /dev/null +++ b/flow/backend/direct/SKILL.md @@ -0,0 +1,36 @@ +--- +name: backend-direct +description: Run backend optimization through NajaEDA Python, Naja-Scope MCP, Kepler Formal MCP and OpenROAD directly, with agent-managed revision files and no 22b flow helper. +--- + +# Direct Backend + +Follow the [backend objectives](../SKILL.md), +[shared session policy](../../session-policy.md) and +[direct revision recipe](../../direct-revisions.md). Do not instantiate a 22b +session helper or use its checkpoint, undo or Scope adapter. The agent performs +the documented steps; no Python flow controller is installed by this skill. + +1. Preserve baseline design, libraries and constraints. Run baseline OpenROAD + and keep the reports before proposing an edit. +2. Select the numbered design file, load it in the separate + [Scope MCP](../../../tools/naja-scope/SKILL.md) server, and inspect connectivity. +3. Review and syntax-check the proposed script. Use the + [NajaEDA Python API](../../../tools/najaeda/SKILL.md) in a fresh candidate + process to load the selected file, edit it and export to a new staging path. + NajaEDA is a Python library here, not a separately configured editing MCP. +4. Call the agent's [Kepler MCP tools](../../../tools/kepler-formal/SKILL.md) + directly on golden versus the exported file, explicitly selecting SEC. + Preserve the structured result, reports, hashes and actual coverage. +5. Publish the revision only after interpreting the proof. Measure it with + [OpenROAD](../../../tools/openroad/SKILL.md) under unchanged settings; record + the revision and hashes with every report. Promote best only on comparable + measured improvement under the recorded objective and proof policy. +6. Restore and reverify the previous retained file when undo is requested. + Refresh Scope and external inputs before discarding the undone checkpoint. + +Use the agent's registered MCP connections, not a hidden notebook flow client. +The [setup guide](../../../setup/README.md) registers Kepler; Scope has its own +installation/client instructions. Direct mode has no automatic edit validator, +mandatory-SEC gate, retention scheduler or crash recovery. The skill requires +those actions but cannot guarantee the agent performed them: retain evidence. diff --git a/flow/backend/managed/SKILL.md b/flow/backend/managed/SKILL.md new file mode 100644 index 0000000..14a7879 --- /dev/null +++ b/flow/backend/managed/SKILL.md @@ -0,0 +1,33 @@ +--- +name: backend-managed +description: Run backend optimization with the 22b Python session helper for cumulative structural edits, checked checkpoints, undo and measured best results. Use for the managed execution flavor, not direct tool orchestration. +--- + +# Managed Backend + +Follow the [backend objectives](../SKILL.md) and +[shared session policy](../../session-policy.md). Use this mode's instructions +only; do not load the direct-mode recipe unless the caller switches modes. + +1. Follow [session startup](../../../tools/live-session.md) to create one + `VersionedDesignSession` in a dedicated Python/Jupyter kernel. Keep golden + unchanged. Configure retention (ten edited checkpoints by default) and the + measurement objective using [session history](../../../tools/session-history.md). +2. Review the NajaEDA script, then call `session.apply_edit(script)`. The helper + validates it, runs live SEC, exports a numbered candidate and runs file SEC. + Keep both proof outcomes and actual coverage; a warning is not full proof. +3. Resolve `session.checkpoint()` for current or an explicit revision for + history. Load that file and `session.libraries` into the separate Scope MCP + server. Use `session.use_checkpoint()` to pin inputs during external runs. +4. Run OpenROAD under the same physical setup. Record actual measurements and + reports with `session.record_measurement(...)`; let the configured objective + select best, never substitute estimated improvements. +5. For undo, use `session.undo()`, not manual database reset or file deletion. + After successful restoration, get `session.mcp_attachment()` again and + reattach external Kepler clients. Refresh Scope to the restored checkpoint. + +A failed edit may leave an unsaved live candidate; repair it or undo to the last +saved checkpoint. Do not treat that checkpoint as the current live state while +the helper reports unsaved changes. Rejected proofs and tool errors stop progress. +The older no-export helper is an explicit compatibility option, not an automatic +fallback when checkpointing fails. diff --git a/flow/direct-revisions.md b/flow/direct-revisions.md new file mode 100644 index 0000000..6e00716 --- /dev/null +++ b/flow/direct-revisions.md @@ -0,0 +1,88 @@ +# Direct Revision Recipe + +This is an agent-executed procedure, not another Python flow helper. Use normal +file operations, reviewed NajaEDA scripts and direct MCP calls. Apply the +[session policy](session-policy.md); do not import the session, history or Scope +adapter modules from 22b to carry out these steps. + +## Start And Record + +Create a private, unused `runs/session_/` directory; include finer time +precision or a unique suffix if needed. Keep immutable `inputs/`, numbered +`versions/revision-0000/` directories, a separate `attempts/` log, and independent +`best/` when a measured winner exists. Initialize a session manifest with mode, +flow, retention (default ten), current revision zero, next attempt number, +objective if supplied, and hashes of original inputs and settings. + +Each published revision records its parent, file hashes, edit script, verification +options, proof result and actual coverage. Include measurement context/report +paths when available. For RTL, include the entire source bundle and frontend +configuration, plus hashes linking generated structural files to those sources. +No particular manifest schema is consumed by the flow helper in direct mode; +choose a clear JSON format and keep it consistent within the session. + +## Edit And Publish + +1. Read the current manifest and verify input hashes. Serialize mutations: do + not edit, switch Scope, undo or prune while another operation uses the design. +2. Reserve a never-reused attempt number and create a fresh staging directory. + Copy the current candidate's inputs, not a stale physical-tool output. Review + and syntax-check the script before executing it. +3. In a fresh candidate-only Python process, load libraries and the selected + structural file with [NajaEDA](../tools/najaeda/SKILL.md), edit and dump to the + staging directory. Golden remains a read-only file, not a mutable peer in + this process. A crash or partial edit leaves current unchanged. +4. Call [Kepler MCP](../tools/kepler-formal/SKILL.md#file-based-verification) + directly on original golden and the dumped candidate, explicitly selecting + SEC. Save the full response, report text and input hashes. Interpret the + actual verdict and coverage; transport success alone is not proof. +5. Only a supported full proof or explicitly labelled non-blocking warning may + publish a structural checkpoint. Keep errors/counterexamples in attempts, + not selectable versions. Write its manifest and rename staging to the final + revision directory, then atomically replace the session's current manifest. + If interrupted, reconcile incomplete publication rather than guessing current. +6. Run external tools on the exact published file and record their hashes with + results. Scope reload and physical measurement are explicit agent actions. + For source-only RTL, retain tests and an explicit SEC-unavailable state, not + a structural checkpoint falsely labelled verified or eligible for proved best. + +## Inspect And Undo + +Resolve current through the manifest, or use the requested retained revision. +In the separate [Scope MCP](../tools/naja-scope/SKILL.md) server, reset only its +own copy, load libraries and the selected Verilog, and confirm top/loaded paths. +Record revision and file hashes with query results. Reuse that loaded copy only +while it still corresponds to the selected immutable files. After a switch or +undo, invalidate the old loaded-revision claim and reload before answering. + +To undo, identify the previous retained checkpoint from the manifest lineage. +After a failed unpublished attempt, keep/restore the existing current checkpoint +instead of discarding it. Check target hashes and reverify its saved design +against original golden in a fresh proof directory. For RTL restore the matching +source bundle too and rerun the applicable checks. In this file-based flavor, +restoration means making this verified file bundle the next tool input; the next +NajaEDA process loads it, and Scope must be refreshed. There is no hidden live +candidate that is magically rolled back. + +After successful validation, update current and refresh Scope; only then remove +the discarded checkpoint. Failed restore leaves current and history unchanged. +Keep failure/proof diagnostics outside the deleted bundle, preserve best, and +never decrement the attempt counter. If a separate live session exists, do not +reuse its old IDs/proofs: an explicit handoff is needed, not a silent mode switch. + +## Retention And Best + +After publishing, prune only this session's superseded edited checkpoints beyond +the configured limit. Baseline, current, in-use files and best must survive. Undo +may skip pruned revisions; make the selected retained parent explicit. + +For best, compare actual reports under identical constraints, libraries, corner, +tool versions, frontend/physical flow and relevant seed/thread settings. Apply +the recorded objective and bounds. Reject absent/nonfinite metrics and missing +evidence. Copy the winning bundle independently to a temporary best directory, +validate its hashes, then replace best and its metadata; do not use a symlink +to a prunable checkpoint. Failed replacement must leave the previous best usable. + +The regression exercises this recipe on a small structural fixture using real +NajaEDA, Scope MCP and Kepler MCP. It is not an agent-reasoning evaluation or +evidence of behavioral RTL synthesis support. diff --git a/flow/rtl/SKILL.md b/flow/rtl/SKILL.md index c10f337..8a27418 100644 --- a/flow/rtl/SKILL.md +++ b/flow/rtl/SKILL.md @@ -5,6 +5,17 @@ description: Author or modify RTL with explicit interface and cycle-level behavi # RTL Design +Select one execution flavor: + +- [Managed](managed/SKILL.md): use the Python session helper for the supported + structural-edit stage, with automatic SEC, saved revisions and undo. +- [Direct](direct/SKILL.md): coordinate the tools and revision files yourself, + without the flow helper, including source-level RTL work. + +Use managed by default for iterative structural work, or honor the requested +mode. Neither mode adds a synthesis frontend or widens a tool's input support. +The [session policy](../session-policy.md) applies to both. + Read the [parent contract](../../SKILL.md). Establish the interface, clock/reset behavior, widths, signedness, latency, throughput and parameter configuration. diff --git a/flow/rtl/direct/SKILL.md b/flow/rtl/direct/SKILL.md new file mode 100644 index 0000000..0404cad --- /dev/null +++ b/flow/rtl/direct/SKILL.md @@ -0,0 +1,38 @@ +--- +name: rtl-direct +description: Coordinate RTL revisions, frontend runs and supported structural inspection and SEC directly through tools, without the 22b session helper. Preserve source-to-structural provenance and explicit verification limits. +--- + +# Direct RTL + +Follow [RTL design guidance](../SKILL.md), +[shared session policy](../../session-policy.md) and +[direct revision recipe](../../direct-revisions.md). Do not instantiate the +22b flow helper, including for checkpoint selection or undo. + +1. Save the original RTL and exact file list, parameters, includes, defines, + top, clock/reset and frontend settings. Keep candidate source files in a + separate numbered workspace. Review source edits and run the chosen RTL + parser/linter and simulation tests directly. +2. Use an explicitly configured frontend when structural tools are needed. + Preserve the command, version, source hashes and generated structural files + for reference and candidate. No synthesis package is supplied by this mode. +3. Inspect supported structural files with + [Scope MCP](../../../tools/naja-scope/SKILL.md). If structurally editing them, + use [NajaEDA Python](../../../tools/najaeda/SKILL.md) in a separate candidate + process. A structural rewrite does not automatically update the RTL source. +4. Call [Kepler MCP](../../../tools/kepler-formal/SKILL.md) directly for SEC on + supported structural reference/candidate files. State exactly which objects + were verified and how they relate to the RTL. Unsupported elaboration or + latency changes are blockers, not warning-level successful proofs. +5. Record source and structural revision identities, actual proof coverage, + tests and measurements. Apply retention and best selection to complete + bundles, not a netlist detached from its source/configuration. +6. Undo by selecting a previous retained bundle, restoring its source and + structural artifacts together, rerunning applicable checks, and refreshing + Scope. Discard the latest version only after the restore is validated. + +For source-only work without a supported frontend, keep lint/simulation evidence +and explicitly mark structural SEC unavailable; do not imply equivalence. Keep +new-design functional tests distinct from reference-based verification. When +handing off to backend, keep direct mode unless the caller requests a switch. diff --git a/flow/rtl/managed/SKILL.md b/flow/rtl/managed/SKILL.md new file mode 100644 index 0000000..9cdb73a --- /dev/null +++ b/flow/rtl/managed/SKILL.md @@ -0,0 +1,34 @@ +--- +name: rtl-managed +description: Coordinate RTL development with a helper-managed structural-edit stage, retaining original RTL and elaboration context while using checked checkpoints and undo where the installed tools support the representation. +--- + +# Managed RTL + +Follow [RTL design guidance](../SKILL.md) and +[shared session policy](../../session-policy.md). This mode does not make the +session helper a behavioral RTL editor or supply an implicit synthesis tool. + +1. Preserve the reference RTL, file list, parameters, includes, defines, top, + clocks/resets and the selected frontend configuration. Run the chosen RTL + lint/simulation checks for source edits; retain source revision hashes. +2. When an explicitly configured frontend produces a supported structural + reference, follow [session startup](../../../tools/live-session.md) and + create `VersionedDesignSession`. Associate its baseline with the source and + frontend hashes. If no supported structural representation exists, report + the blocked helper/SEC stage; do not invent an RTL proof or switch modes. +3. Review a NajaEDA `edit(top)` script and call `session.apply_edit(script)`. + Keep live and checkpoint SEC outcomes, coverage and the correspondence to + the RTL source. The helper operates on structural objects, not source text. +4. Inspect selected checkpoints with Scope. Use `session.undo()` to restore a + structural revision, then refresh Scope and external Kepler attachments. + This does not undo RTL files, rerun elaboration or recover source code. +5. A later source-level RTL change needs matching frontend settings and a new + traceable structural candidate; do not reload it behind the helper or use a + proof of an earlier structural edit as proof of the new RTL. Preserve the + original reference and verify each candidate against it. + +Use [session history](../../../tools/session-history.md) for retention and best +measurements. Delegate physical measurements to the backend flow with the same +managed choice. A design with no reference needs functional tests; it cannot +gain a specification-equivalence claim through self-comparison. diff --git a/flow/session-policy.md b/flow/session-policy.md new file mode 100644 index 0000000..ca0021f --- /dev/null +++ b/flow/session-policy.md @@ -0,0 +1,37 @@ +# Session Policy For Both Modes + +These are shared rules, not executable enforcement. Managed mode implements +structural checkpoint operations in its helper; direct mode follows the +[file-based recipe](direct-revisions.md) through agent tool calls. + +- Keep original golden, constraints, libraries and tool/frontend settings + immutable and hashed. Candidate history is never a replacement for golden. +- Use a unique dated session directory and numbered revisions. Reserve a fresh + increasing number for each edit attempt; failures and undo never reuse it. + Keep an explicit current revision, not a newest-timestamp guess. +- Save baseline revision zero permanently. Default retention is ten recent + edited checkpoints, configurable per session. Keep inputs being used by an + external tool, baseline and an independent best copy out of pruning. +- Review and syntax-check edits before execution. Record real SEC outcome and + coverage for each supported edited design. Exported files need their own + verification; a live proof does not certify Verilog serialization. +- Partial or inconclusive proofs with usable coverage remain explicitly + unproven warnings. Counterexamples, zero usable coverage, tool errors and + timeouts stop the candidate flow. Never publish missing evidence as success. +- Undo restores the preceding retained version (or the last saved version + after an unsaved failed attempt). Verify restoration before deleting the + discarded checkpoint. Invalidate obsolete Scope observations, proofs and + live design references. Never reset a universe holding golden to undo candidate. +- Keep each measurement tied to the exact revision, input hashes and physical + context. Select best by a recorded objective and bounds, not by intuition. + Full exported proof is required for promotion by default; any explicit + allowance for unproven results must remain visible in best's metadata. +- Best is an independent bundle of design, proof, measurements and provenance; + it survives undo and rolling retention. Without an objective, do not invent + one or automatically select best. A changed objective/setup starts a new + comparison rather than mixing incomparable results. + +For RTL, also preserve source files and their correspondence to elaborated +structural artifacts. Helper undo covers only the structural candidate; direct +bundle restoration must include source/configuration. Report unavailable +frontend/SEC stages explicitly rather than claiming an unsupported RTL proof. diff --git a/scripts/direct_tools_regression.py b/scripts/direct_tools_regression.py new file mode 100644 index 0000000..83a33b0 --- /dev/null +++ b/scripts/direct_tools_regression.py @@ -0,0 +1,250 @@ +"""Real file-based edit/inspect/SEC/undo without importing 22b flow helpers. + +This is a deterministic structural fixture replay, not an agent implementation +or an RTL elaboration test. Only stdlib and the installed tool APIs are used. +""" + +import argparse +import ast +import asyncio +from contextlib import asynccontextmanager +import hashlib +import json +import os +from pathlib import Path +import shutil +import subprocess +import sys + + +LIBERTY = '''library(cells) { + cell(BUF) { pin(A) { direction: input; } + pin(Y) { direction: output; function: "A"; } } + cell(INV) { pin(A) { direction: input; } + pin(Y) { direction: output; function: "!A"; } } +} +''' +BASELINE = '''module top(input a, output y); +wire stage; +BUF g(.A(a), .Y(stage)); +BUF h(.A(stage), .Y(y)); +endmodule +''' +EDIT = '''from najaeda import netlist +import sys + +netlist.load_liberty([sys.argv[1]]) +top = netlist.load_verilog([sys.argv[2]]) +assert top is not None +old = top.get_child_instance("h") +driver = top.get_child_instance("g") +assert old is not None and driver is not None +output = old.get_term("Y").get_upper_net() +driver.get_term("Y").connect_upper_net(output) +old.delete() +top.dump_verilog(sys.argv[3]) +''' + + +def save(path, value): + temporary = path.with_suffix(".tmp") + temporary.write_text(json.dumps(value, indent=2, allow_nan=False) + "\n") + temporary.replace(path) + + +def digest(path): + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def payload(reply): + if reply.isError: + raise ValueError("MCP tool error") + texts = [item.text for item in reply.content if item.type == "text"] + if len(texts) != 1: + raise ValueError("Missing unambiguous MCP response") + value = json.loads(texts[0]) + if not isinstance(value, dict) or value.get("status") == "error" or value.get("error"): + raise ValueError("Tool returned an error or malformed result") + return value + + +def require_proof(result, different=False): + proof = result.get("verification_result", {}) + verdict = "different" if different else "equivalent" + if (result.get("status") != "success" or result.get("verdict") != verdict + or proof.get("status") != verdict or proof.get("verification") != "sec" + or type(result.get("exit_code")) is not int + or proof.get("exit_code") != result["exit_code"]): + raise ValueError("Missing or contradictory SEC outcome") + if not different and (result["exit_code"] != 0 + or any(type(proof.get(k)) is not int or proof[k] != 1 + for k in ("total_outputs", "covered_outputs", "proven_outputs")) + or proof.get("coverage_percent") != 100 + or proof.get("equivalent") is not True or proof.get("conclusive") is not True + or proof.get("unproven_outputs") != [] or proof.get("skipped_observed_outputs") != []): + raise ValueError("Fixture requires full one-output SEC proof") + reports = result.get("reports") + expected = {"skipped_multi_driver_pos.txt", "skipped_no_driver_pos.txt", + "skipped_logical_loop_pos.txt"} + if (not isinstance(reports, dict) or set(reports) != expected + or not all(isinstance(text, str) for text in reports.values()) + or (not different and any(text.strip() for text in reports.values()))): + raise ValueError("Missing or contradictory extraction reports") + + +@asynccontextmanager +async def server(module, work): + from mcp import ClientSession, StdioServerParameters + from mcp.client.stdio import stdio_client + + work.mkdir() + env = dict(os.environ) + for key in ("PYTHONPATH", "PYTHONHOME", "NAJAEDA_SRC", "EQUIVALENCE_CHECK"): + env.pop(key, None) + env.update(NAJA_SCOPE_ENABLE_PYTHON="0", KEPLER_FORMAL_AI_OUTPUT_DIR=str(work)) + params = StdioServerParameters(command=sys.executable, args=["-m", module], + cwd=str(work), env=env) + with (work / "server.log").open("w") as log: + async with stdio_client(params, errlog=log) as streams: + async with ClientSession(*streams) as client: + await client.initialize() + save(work / "schemas.json", (await client.list_tools()).model_dump(mode="json")) + yield client + + +async def run(work): + work.mkdir(parents=True, exist_ok=False) + inputs = work / "inputs" + inputs.mkdir() + golden, library = inputs / "golden.v", inputs / "cells.lib" + golden.write_text(BASELINE) + library.write_text(LIBERTY) + golden.chmod(0o400) + library.chmod(0o400) + hashes = {str(p): digest(p) for p in (golden, library)} + baseline = work / "versions/revision-0000" + baseline.mkdir(parents=True) + shutil.copyfile(golden, baseline / "design.v") + state = {"mode": "direct", "current": 0, "next_attempt": 1, "retention": 10, + "input_hashes": hashes, "objective": "minimize measured instance count (not PPA)"} + save(work / "session.json", state) + async with server("kepler_formal_mcp", work / "kepler") as formal, \ + server("naja_scope.server", work / "scope") as scope: + info = payload(await formal.call_tool("get_kepler_formal_info", {})) + if info.get("status") != "success": + raise ValueError("Native Kepler capability check failed") + save(work / "kepler-info.json", info) + + async def prove(label, candidate, different=False): + output = work / label + output.mkdir() + request = {"input_paths": [str(golden), str(candidate)], + "liberty_files": [str(library)], "allowed_output_dir": str(output), + "verification": "sec", "solver": "kissat", "max_k": 32, + "sec_engine": "pdr", "sec_encoding": "dual_rail_steady", + "allow_boundary_mismatch": False, "report_skipped_outputs": True, + "cnf_export": False, "timeout_seconds": 60, + "yaml_output_path": "config.yaml", "log_file_name": "kepler.log"} + save(output / "request.json", request) + before = {str(p): digest(p) for p in (golden, library, candidate)} + reply = await formal.call_tool("create_yaml_and_run_kepler_formal", request) + save(output / "mcp-result.json", reply.model_dump(mode="json")) + result = payload(reply) + save(output / "result.json", result) + require_proof(result, different) + if before != {str(p): digest(p) for p in (golden, library, candidate)}: + raise ValueError("Verification changed its inputs") + save(output / "input-hashes.json", before) + return result + + async def inspect(label, design): + payload(await scope.call_tool("reset_universe", {})) + payload(await scope.call_tool("load_liberty", {"files": [str(library)]})) + payload(await scope.call_tool("load_verilog", {"files": [str(design)]})) + status = payload(await scope.call_tool("status", {})) + if (not status.get("loaded") or status.get("top", {}).get("name") != "top" + or str(design) not in status.get("loaded_files", [])): + raise ValueError("Scope loaded a different design") + response = payload(await scope.call_tool("find", { + "pattern": "*", "kind": "instance", "limit": 100})) + if response.get("has_more") or response.get("truncated"): + raise ValueError("Incomplete Scope observations") + names = sorted(item["path"] for item in response["matches"]) + save(work / f"scope-{label}.json", {"input_sha256": digest(design), + "status": status, "response": response}) + return names + + original = await inspect("baseline", baseline / "design.v") + await prove("baseline-proof", baseline / "design.v") + if original != ["top.g", "top.h"]: + raise ValueError("Unexpected baseline connectivity") + staging = work / "attempt-0001" + staging.mkdir() + script = staging / "edit.py" + script.write_text(EDIT) + ast.parse(EDIT) # Reviewed fixture code; direct mode has no helper validator. + candidate = staging / "design.v" + state["next_attempt"] = 2 + save(work / "session.json", state) + env = dict(os.environ) + env.pop("PYTHONPATH", None) + env.pop("NAJAEDA_SRC", None) + with (staging / "edit.log").open("w") as log: + subprocess.run([sys.executable, str(script), str(library), str(baseline / "design.v"), + str(candidate)], cwd=staging, env=env, stdout=log, + stderr=subprocess.STDOUT, check=True, timeout=60) + proof = await prove("edit-proof", candidate) + save(staging / "manifest.json", {"revision": 1, "parent": 0, + "sha256": digest(candidate), "proof": proof}) + edited = work / "versions/revision-0001" + staging.rename(edited) + state["current"] = 1 + save(work / "session.json", state) + after = await inspect("edited", edited / "design.v") + if after != ["top.g"]: + raise ValueError("Scope did not observe the direct edit") + # Real structural measurement, explicitly not an area/timing claim. + save(edited / "measurement.json", {"instance_count": len(after), + "baseline_instance_count": len(original), "evidence": "scope-edited.json"}) + shutil.copytree(edited, work / "best") + shutil.copyfile(work / "scope-edited.json", work / "best/scope-edited.json") + best_hash = digest(work / "best/design.v") + await inspect("historical", baseline / "design.v") + if await inspect("current", edited / "design.v") != after: + raise ValueError("Scope failed to switch back to current") + wrong = work / "attempt-0002" + wrong.mkdir() + (wrong / "design.v").write_text("module top(input a, output y); INV bad(.A(a), .Y(y)); endmodule\n") + await prove("counterexample-proof", wrong / "design.v", different=True) + state["next_attempt"] = 3 + save(work / "session.json", state) + if state["current"] != 1: + raise ValueError("Rejected edit changed current") + await prove("restore-proof", baseline / "design.v") + restored = await inspect("restored", baseline / "design.v") + if restored != original: + raise ValueError("Undo did not restore Scope observations") + state["current"] = 0 + save(work / "session.json", state) + shutil.rmtree(edited) # Only our isolated, now discarded test checkpoint. + if digest(work / "best/design.v") != best_hash: + raise ValueError("Undo corrupted best") + if hashes != {str(p): digest(p) for p in (golden, library)}: + raise ValueError("Golden or libraries changed") + forbidden = {"tools.live_session", "tools.versioned_session", "tools.session_history", + "tools.scope_checkpoints"} + if forbidden & set(sys.modules): + raise ValueError("Direct replay imported a flow helper") + save(work / "result.json", {"status": "passed", "flow_helper_imports": [], + "scope_before": original, "scope_after": after, "scope_restored": restored, + "full_sec_outputs": 1, "counterexample_rejected": True, "best_preserved": True, + "current": state["current"], "next_attempt": state["next_attempt"], + "rtl_elaboration_tested": False, "model_reasoning_tested": False}) + print("PASS: helper-free NajaEDA edit, Scope switching, SEC, counterexample and undo", flush=True) + + +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=300)) diff --git a/scripts/gcd_undo_regression.py b/scripts/gcd_undo_regression.py new file mode 100644 index 0000000..3512f4a --- /dev/null +++ b/scripts/gcd_undo_regression.py @@ -0,0 +1,175 @@ +"""Packaged GCD baseline -> edit -> undo, with real Scope, SEC and OpenROAD.""" + +import argparse +import ast +import asyncio +import json +from pathlib import Path +import sys + +ROOT = Path(__file__).resolve().parents[1] +sys.path.insert(0, str(ROOT)) + +from scripts import gcd_reference_regression as reference +from tools.live_session import _McpClient, SEC +from tools.scope_checkpoints import ScopeCheckpoints +from tools.versioned_session import VersionedDesignSession + + +class ScopeClient(_McpClient): + async def _serve(self): + from mcp import ClientSession, StdioServerParameters + from mcp.client.stdio import stdio_client + + params = StdioServerParameters(command=sys.executable, args=["-m", "naja_scope.server"], + env=reference.clean_env(), cwd=str(ROOT)) + with (self.directory / "scope-server.log").open("w") as log: + async with stdio_client(params, errlog=log) as streams: + async with ClientSession(*streams) as session: + await asyncio.wait_for(session.initialize(), 30) + schemas = await session.list_tools() + reference.save(self.directory / "scope-tools.json", schemas.model_dump(mode="json")) + self.ready.set_result({tool.name for tool in schemas.tools}) + index = 0 + while True: + request = await asyncio.to_thread(self.requests.get) + if request is None: + return + name, arguments, future = request + try: + response = await session.call_tool(name, arguments) + index += 1 + reference.save(self.directory / f"scope-{index:04d}.json", { + "tool": name, "arguments": arguments, + "response": response.model_dump(mode="json")}) + future.set_result(reference.scope_payload(response)) + except Exception as error: + future.set_exception(error) + + +def observations(scope, revision=None): + result = {} + for name, pattern in (("original_gates", "_21[5-9]_"), ("replacement_gates", "ppa_cla_*")): + response = scope.query("find", {"pattern": pattern, "kind": "instance", "limit": 200}, + revision=revision)["result"] + if response.get("has_more") or response.get("truncated"): + raise ValueError("Scope query did not cover the complete replacement boundary") + result[name] = sorted(response["matches"], key=lambda item: item["path"]) + # An unchanged downstream net exposes the changed driver, not just cell counts. + result["boundary"] = scope.query("get_drivers", {"path": "gcd._057_", "limit": 200}, + revision=revision)["result"] + if result["boundary"].get("truncated"): + raise ValueError("Truncated Scope connectivity evidence") + return result + + +def require_restored(baseline, restored): + # Identical bytes, package and setup: demand the same results, not improvement. + for key in ("setup_ns", "hold_ns", "tns_ns", "area_um2", "routing_drc", "power_report"): + if baseline[key] != restored[key]: + raise ValueError(f"Restored OpenROAD result differs from baseline: {key}") + + +def live_cells(session): + # Check actual live objects too: selecting an old file alone is not undo. + with session._inspection_access(): + return sorted((cell.getName(), cell.getModel().getName()) + for cell in session._candidate.getInstances()) + + +def run(work, fixture, timeout): + metadata = reference.prepare(work, fixture) + liberty = fixture / "test/sky130hd/sky130hd_tt.lib" + script_tree = ast.parse((reference.REFERENCE / "edit.py").read_text()) + script = ast.unparse(ast.Module(body=[n for n in script_tree.body if isinstance(n, ast.FunctionDef)], + type_ignores=[])) + objective = {"weights": {"setup_ns": -1}, + "bounds": {"hold_ns": {"min": 0}, "routing_drc": {"max": 0}}} + session = VersionedDesignSession(work / "inputs/input.v", [liberty], sessions_root=work, + objective=objective, timeout=timeout) + client = None + try: + client = ScopeClient(work, timeout) + scope = ScopeCheckpoints(session, client.call) + golden_hash = session.status()["golden_sha256"] + baseline_cells = live_cells(session) + original_attachment = session.mcp_attachment() + context = {"openroad": metadata["openroad_version"], + "sdc": reference.digest(work / "inputs/constraints.sdc"), + "flow": reference.digest(reference.PLATFORM / "run.tcl"), + "fixture": metadata["fixture_manifest_sha256"]} + + def physical(label, measure=True): + print(f"OpenROAD: {label}", flush=True) + directory = work / label + with session.use_checkpoint() as checkpoint: + SEC.require_full(checkpoint["export_proof"], reference.EXPECTED_OUTPUTS) + env = reference.clean_env() + env.update(GCD_RUN_DIR=str(directory), GCD_TEST_DIR=str(fixture / "test"), + GCD_INPUT=checkpoint["verilog_file"], GCD_SDC=str(work / "inputs/constraints.sdc")) + reference.run_command(directory, [metadata["tools"]["openroad"], "-no_init", "-exit", "-metrics", + str(directory / "metrics.json"), str(reference.PLATFORM / "run.tcl")], + timeout=timeout, env=env) + summary = reference.physical_summary(directory) + reference.save(directory / "summary.json", dict(summary, revision=checkpoint["revision"], + input_sha256=checkpoint["files"]["design.v"])) + if measure: + session.record_measurement({k: v for k, v in summary.items() if k != "power_report"}, + context=context, evidence=[directory / "summary.json", + directory / "metrics.json", directory / "reports/power.rpt"]) + return summary + + print("Naja-Scope: baseline revision zero", flush=True) + before = observations(scope) + assert len(before["original_gates"]) == 5 and not before["replacement_gates"] + baseline = physical("baseline") + print("NajaEDA: reference edit, live SEC, checkpoint SEC", flush=True) + SEC.require_full(session.apply_edit(script), reference.EXPECTED_OUTPUTS) + assert live_cells(session) != baseline_cells + edited = session.checkpoint() + after = observations(scope) + assert not after["original_gates"] and len(after["replacement_gates"]) == 31 + assert before["boundary"] != after["boundary"] + assert observations(scope, revision=0) == before # Explicit historical selection. + assert observations(scope) == after # Default returns to current. + candidate = physical("candidate") + gain = reference.compare(baseline, candidate) + assert session.history.best["revision"] == edited["revision"] + best_hash = reference.digest(session.directory / "best/design.v") + print("Undo: restore previous netlist, SEC, then delete discarded revision", flush=True) + undo = session.undo() + SEC.require_full(undo["proof"], reference.EXPECTED_OUTPUTS) + assert undo["restored_revision"] == 0 + assert not Path(edited["directory"]).exists() + assert session.status()["golden_sha256"] == golden_hash + assert live_cells(session) == baseline_cells + assert session.mcp_attachment()["session_id"] != original_attachment["session_id"] + assert reference.digest(session.directory / "best/design.v") == best_hash + restored_observations = observations(scope) + assert restored_observations == before + restored = physical("restored", measure=False) + require_restored(baseline, restored) + assert session.checkpoint()["files"]["design.v"] == reference.digest(work / "inputs/input.v") + reference.validate_inputs(work, metadata) + reference.save(work / "scope-comparison.json", {"baseline": before, "candidate": after, + "restored": restored_observations}) + reference.save(work / "comparison.json", dict(gain, restored=restored, undo=undo, + status="passed", scope_restored=True, physical_restored=True, + live_candidate_restored=True, best_preserved=True, discarded_netlist_deleted=True)) + print(f"PASS: Scope and OpenROAD restored; edit gained {gain['setup_gain_ns']:.9f} ns; " + "18/18 outputs proved after edit and undo", flush=True) + finally: + if client is not None: + client.close() + session.close() + + +if __name__ == "__main__": + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--work-dir", type=Path, required=True) + parser.add_argument("--fixture-dir", type=Path, default=ROOT / ".cache/gcd-fixture-v2") + parser.add_argument("--timeout-seconds", type=int, default=600) + args = parser.parse_args() + if args.timeout_seconds <= 0: + parser.error("--timeout-seconds must be positive") + run(args.work_dir.resolve(), args.fixture_dir.resolve(), args.timeout_seconds) diff --git a/scripts/versioned_session_regression.py b/scripts/versioned_session_regression.py new file mode 100644 index 0000000..757d9da --- /dev/null +++ b/scripts/versioned_session_regression.py @@ -0,0 +1,158 @@ +"""Real packaged-tool history guards, independent of the physical GCD run.""" + +import argparse +import json +from pathlib import Path +import sys +import tempfile +import time +from unittest.mock import patch + +ROOT = Path(__file__).resolve().parents[1] +sys.path.insert(0, str(ROOT)) + +from scripts.live_session_regression import LIBERTY, FIRST, SECOND, DIFFERENT +from scripts.gcd_undo_regression import ScopeClient +from tools.scope_checkpoints import ScopeCheckpoints +from tools.versioned_session import VersionedDesignSession +from tools.live_session import SEC + + +def run(work): + 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) + with VersionedDesignSession(source, [library], sessions_root=work, retention=2) as session: + client = ScopeClient(work, 120) + scope = ScopeCheckpoints(session, client.call) + try: + def gates(): + response = scope.query("find", {"pattern": "*", "kind": "instance", "limit": 200}) + return sorted(item["path"] for item in response["result"]["matches"]) + + initial = gates() + original = session.mcp_attachment() + for script in (FIRST, SECOND): + assert session.apply_edit(script)["proved_outputs"] == 1 + assert gates() == ["top.g", "top.h1", "top.h2"] + checkpoint_before_error = session.checkpoint() + with patch.object(SEC, "run_sec", side_effect=RuntimeError("simulated export check failure")): + try: + session.apply_edit('def edit(top):\n top.create_net("unsaved")\n') + except RuntimeError as error: + assert "simulated export" in str(error) + else: + raise AssertionError("Failed checkpoint was published") + assert session.status()["netlist_revision"] is None + assert session.history.active == checkpoint_before_error["revision"] + assert session.undo()["restored_revision"] == 2 + try: + session.apply_edit(DIFFERENT) + except ValueError as error: + assert "counterexample" in str(error) + else: + raise AssertionError("Counterexample accepted") + try: + session.checkpoint() + except RuntimeError: + pass + else: + raise AssertionError("Stale checkpoint claimed as current") + # A failed edit restores the last saved version, without discarding it. + assert session.undo()["restored_revision"] == 2 + assert gates() == ["top.g", "top.h1", "top.h2"] + before_failed_undo = session.status() + with patch.object(SEC, "run_sec", side_effect=RuntimeError("simulated restore proof failure")): + try: + session.undo() + except RuntimeError: + pass + else: + raise AssertionError("Undo ignored its failed file check") + assert session.status() == before_failed_undo + assert Path(session.checkpoint()["verilog_file"]).exists() + assert session.undo()["restored_revision"] == 1 + assert gates() == ["top.g", "top.h"] + assert session.undo()["restored_revision"] == 0 + assert gates() == initial + assert session.mcp_attachment()["session_id"] != original["session_id"] + stale = session._client.call("verify_session", { + "session_id": session.mcp_attachment()["session_id"], + "design1": original["design1"], "design2": original["design2"], "verification": "sec"}) + assert stale["status"] == "error" # Native IDs may match; binding identity cannot. + assert session.apply_edit(FIRST)["revision"] == 5 # Never reuse discarded IDs. + assert gates() == ["top.g", "top.h"] + for number in range(3): + session.apply_edit(f'def edit(top):\n top.create_net("unused{number}")\n') + assert sorted(session.history.records) == [0, 7, 8] + session.configure_history(retention=1) + assert sorted(session.history.records) == [0, 8] + artifact = session.checkpoint() + Path(artifact["verilog_file"]).write_text("corrupt export") + before = session.status() + try: + session.checkpoint() + except ValueError: + pass + else: + raise AssertionError("Modified checkpoint accepted") + assert session.status() == before # Disk tampering never mutates live golden/candidate. + (work / "result.json").write_text(json.dumps({"status": "passed", "retention": True, + "undo": True, "scope_refresh": True, "counterexample_rejected": True, + "failed_edit_recovered": True, "stale_native_reference_rejected": True, + "failed_checkpoint_unpublished": True, "failed_undo_nondestructive": True, + "post_undo_edit": True, "modified_checkpoint_rejected": True}, indent=2) + "\n") + print("PASS: real SEC, Scope, undo, retention, continued edits and stale-ID rejection", flush=True) + finally: + client.close() + + +def run_notebook(work): + from jupyter_client import KernelManager + from scripts.gcd_reference_regression import clean_env + + work.mkdir(parents=True, exist_ok=False) + with tempfile.TemporaryDirectory(prefix="22b-history-kernel-", dir="/tmp") as private: + manager = KernelManager(transport="ipc", connection_file=str(Path(private) / "connection.json")) + manager.kernel_spec.argv = [sys.executable, "-m", "ipykernel_launcher", "-f", "{connection_file}"] + manager.start_kernel(cwd=str(ROOT), env=clean_env()) + client = manager.blocking_client() + client.start_channels() + try: + client.wait_for_ready(timeout=30) + code = ("from pathlib import Path\nfrom scripts.versioned_session_regression import run\n" + f"run(Path({str(work / 'native')!r}))\n") + (work / "cell.py").write_text(code) + request = client.execute(code, store_history=False, allow_stdin=False) + deadline = time.monotonic() + 600 + error = None + with (work / "kernel.log").open("w") as log: + while True: + message = client.get_iopub_msg(timeout=max(0.1, deadline - time.monotonic())) + if message.get("parent_header", {}).get("msg_id") != request: + continue + kind, content = message["msg_type"], message["content"] + if kind == "stream": + log.write(content["text"]) + elif kind == "error": + error = content["ename"] + ": " + content["evalue"] + log.write(error + "\n") + elif kind == "status" and content["execution_state"] == "idle": + break + if error: + raise RuntimeError(error) + if json.loads((work / "native/result.json").read_text())["status"] != "passed": + raise RuntimeError("Missing successful notebook history result") + print("PASS: versioned history, Scope and SEC inside a real Jupyter kernel", flush=True) + finally: + client.stop_channels() + manager.shutdown_kernel(now=True) + + +if __name__ == "__main__": + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--work-dir", required=True, type=Path) + parser.add_argument("--jupyter", action="store_true") + args = parser.parse_args() + (run_notebook if args.jupyter else run)(args.work_dir.resolve()) diff --git a/setup/README.md b/setup/README.md index 7983991..f24c998 100644 --- a/setup/README.md +++ b/setup/README.md @@ -60,10 +60,24 @@ 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 +## Choose How To Use The Tools -Start the [persistent session](../tools/live-session.md) in a dedicated kernel -using this same environment. In that kernel: +Registration works for both flow flavors. **Direct mode** uses the agent's +registered Kepler file-based tools with golden/candidate paths; it does not +instantiate the flow helper or attach to its session. Follow the selected +backend/RTL direct skill and [Kepler operations](../tools/kepler-formal/SKILL.md). +Register [Scope](../tools/naja-scope/install.md) separately when needed; this +setup command does not register Scope or an editing MCP for NajaEDA. + +The attachment procedure below is for **managed mode** (or an explicitly +provided compatible live owner), not a prerequisite for all MCP usage. + +## Attach To Managed Live Designs + +For managed mode, start `VersionedDesignSession` from the +[session startup example](../tools/live-session.md) in a dedicated kernel using +this same environment. It owns automatic checkpoints and undo as well as live +SEC. In that kernel: ```python attachment = session.mcp_attachment() @@ -88,6 +102,11 @@ MCP aliases. Keep edits and direct proofs sequential. Recheck must still match the ones observed before it. A proof for an older revision does not certify the current candidate. +After `session.undo()`, fetch a new attachment and repeat the attachment steps +above: undo expires the previous binding even if native design IDs are reused. +The attempt counter never rewinds; `session.status()["netlist_revision"]` +identifies the restored saved version. Do not reuse pre-undo references. + 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. diff --git a/tests/test_flow_modes.py b/tests/test_flow_modes.py new file mode 100644 index 0000000..88f0548 --- /dev/null +++ b/tests/test_flow_modes.py @@ -0,0 +1,95 @@ +"""Mode discovery, dependency boundaries and direct-replay evidence guards.""" + +import ast +import copy +from pathlib import Path +import re +import unittest + +from scripts.direct_tools_regression import EDIT, require_proof +from test_gcd_reference_regression import proof_result + + +ROOT = Path(__file__).resolve().parents[1] + + +def links(path): + return {(path.parent / target.split("#", 1)[0]).resolve() + for target in re.findall(r"\[[^\]]*\]\(([^)]+)\)", path.read_text()) + if "://" not in target and not target.startswith("#")} + + +class ModeTests(unittest.TestCase): + def test_both_applications_route_to_both_local_flavors(self): + shared = ROOT / "flow/session-policy.md" + for flow in ("backend", "rtl"): + entry = ROOT / f"flow/{flow}/SKILL.md" + for mode in ("managed", "direct"): + skill = ROOT / f"flow/{flow}/{mode}/SKILL.md" + with self.subTest(flow=flow, mode=mode): + self.assertTrue(skill.is_file()) + self.assertIn(skill, links(entry)) + self.assertIn(entry, links(skill)) + self.assertIn(shared, links(skill)) + + def test_direct_guides_share_recipe_not_managed_startup(self): + for flow in ("backend", "rtl"): + skill = ROOT / f"flow/{flow}/direct/SKILL.md" + direct_links = links(skill) + self.assertIn(ROOT / "flow/direct-revisions.md", direct_links) + self.assertNotIn(ROOT / "tools/live-session.md", direct_links) + self.assertNotIn(ROOT / "tools/session-history.md", direct_links) + for tool in ("najaeda", "naja-scope", "kepler-formal"): + self.assertIn(ROOT / f"tools/{tool}/SKILL.md", direct_links) + + def test_managed_guides_select_tested_owner(self): + for flow in ("backend", "rtl"): + skill = ROOT / f"flow/{flow}/managed/SKILL.md" + self.assertIn(ROOT / "tools/live-session.md", links(skill)) + self.assertIn(ROOT / "tools/session-history.md", links(skill)) + + def test_direct_runner_has_no_flow_helper_dependencies(self): + path = ROOT / "scripts/direct_tools_regression.py" + tree = ast.parse(path.read_text()) + for node in ast.walk(tree): + modules = ([node.module] if isinstance(node, ast.ImportFrom) else + [alias.name for alias in node.names] if isinstance(node, ast.Import) else []) + for module in modules: + self.assertNotIn(module.split(".")[0], {"tools", "scripts", "flow"}) + candidate = ast.parse(EDIT) + imports = [n.module for n in ast.walk(candidate) if isinstance(n, ast.ImportFrom)] + self.assertEqual(imports, ["najaeda"]) + + def test_direct_fixture_requires_real_full_proof(self): + result = proof_result(total=1, covered=1, proven=1) + require_proof(result) + for key, value in (("verification", "lec"), ("proven_outputs", 0), + ("covered_outputs", 0), ("total_outputs", 0), + ("conclusive", False), ("skipped_observed_outputs", ["y"])): + bad = copy.deepcopy(result) + bad["verification_result"][key] = value + with self.subTest(key=key), self.assertRaises(ValueError): + require_proof(bad) + for status in ("partially_proved", "inconclusive", "different"): + with self.assertRaises(ValueError): + require_proof(proof_result(status, total=1, covered=1, proven=0)) + + def test_counterexample_is_distinguished_from_execution_error(self): + different = proof_result("different", total=1, covered=1, proven=0) + require_proof(different, different=True) + for bad in ({"status": "error"}, {"status": "success"}, + proof_result(total=1, covered=1, proven=1)): + with self.assertRaises(ValueError): + require_proof(bad, different=True) + + def test_new_workflow_runs_both_real_modes_without_changing_gcd_replay(self): + workflow = (ROOT / ".github/workflows/flow-modes-verify.yml").read_text() + for runner in ("direct_tools_regression.py", "versioned_session_regression.py"): + self.assertIn(runner, workflow) + original = (ROOT / ".github/workflows/gcd-reference-verify.yml").read_text() + self.assertNotIn("direct_tools_regression.py", original) + self.assertIn("if: always()", workflow) + + +if __name__ == "__main__": + unittest.main() diff --git a/tests/test_repository.py b/tests/test_repository.py index 8219df7..6cb78c5 100644 --- a/tests/test_repository.py +++ b/tests/test_repository.py @@ -7,7 +7,7 @@ ROOT = Path(__file__).resolve().parents[1] -SKILLS = [ROOT / "SKILL.md", *sorted((ROOT / "flow").glob("*/SKILL.md")), +SKILLS = [ROOT / "SKILL.md", *sorted((ROOT / "flow").rglob("SKILL.md")), *sorted((ROOT / "tools").glob("*/SKILL.md"))] DOCS = [ROOT / "README.md", ROOT / "AGENTS.md", ROOT / "SKILL.md", *sorted((ROOT / "flow").rglob("*.md")), @@ -39,7 +39,7 @@ def test_demo_has_repository_download_fallback(self): self.assertEqual(stream.read(12)[4:8], b"ftyp") def test_skill_frontmatter(self): - self.assertEqual(len(SKILLS), 7) + self.assertEqual(len(SKILLS), 11) names = set() for path in SKILLS: with self.subTest(path=path.relative_to(ROOT)): diff --git a/tests/test_session_history.py b/tests/test_session_history.py new file mode 100644 index 0000000..0c95adc --- /dev/null +++ b/tests/test_session_history.py @@ -0,0 +1,180 @@ +"""Offline storage/selection guards, not physical or formal verification.""" + +from contextlib import contextmanager +import json +from pathlib import Path +import tempfile +import unittest + +from tools.session_history import RevisionHistory +from tools.scope_checkpoints import ScopeCheckpoints +from scripts.gcd_undo_regression import require_restored + + +class HistoryTests(unittest.TestCase): + def setUp(self): + self.temp = tempfile.TemporaryDirectory() + self.addCleanup(self.temp.cleanup) + self.root = Path(self.temp.name) + self.history = RevisionHistory(self.root) + + def publish(self, revision, status="proved"): + directory = Path(tempfile.mkdtemp(dir=self.root)) + (directory / "design.v").write_text(f"// revision {revision}\nmodule top(); endmodule\n") + return self.history.publish(directory, revision, {"top": "top", "export_proof": {"status": status}}) + + def test_default_ten_recent_edits_plus_preserved_baseline(self): + for i in range(13): + self.publish(i) + self.assertEqual(sorted(self.history.records), [0, *range(3, 13)]) + self.assertEqual(self.history.active, 12) + self.assertEqual(json.loads((self.root / "config.json").read_text())["retention"], 10) + + def test_configurable_retention_and_invalid_values(self): + for i in range(4): + self.publish(i) + for bad in (0, -1, True, 1.5, "10"): + with self.assertRaises(ValueError): + self.history.configure(bad) + self.history.configure(1) + self.assertEqual(sorted(self.history.records), [0, 3]) + + def test_undo_deletes_latest_and_does_not_reuse_numbers(self): + self.publish(0) + latest = self.publish(1) + target = self.history.undo_target() + self.history.finish_undo(target["revision"]) + self.assertEqual(self.history.active, 0) + self.assertFalse(Path(latest["directory"]).exists()) + with self.assertRaises(ValueError): + self.publish(1) + self.publish(2) + self.assertEqual(sorted(self.history.records), [0, 2]) + self.assertEqual(self.history.get()["parent"], 0) + + def test_empty_history_or_baseline_cannot_undo(self): + self.publish(0) + with self.assertRaises(ValueError): + self.history.undo_target() + with self.assertRaises(ValueError): + self.history.get(99) + + def test_inflight_inputs_survive_pruning_and_block_deletion(self): + self.publish(0) + self.publish(1) + self.history.configure(1) + with self.history.acquire(1): + with self.assertRaises(RuntimeError): + self.history.undo_target() + self.publish(2) + self.assertIn(1, self.history.records) + self.assertNotIn(1, self.history.records) + + def test_modified_export_or_manifest_rejected(self): + record = self.publish(0) + path = Path(record["verilog_file"]) + original = path.read_text() + path.write_text("corrupt") + with self.assertRaises(ValueError): + self.history.get() + path.write_text(original) + (Path(record["directory"]) / "manifest.json").write_text("{}") + with self.assertRaises(ValueError): + self.history.get() + + def test_bad_or_empty_snapshot_not_published(self): + directory = Path(tempfile.mkdtemp(dir=self.root)) + with self.assertRaises(ValueError): + self.history.publish(directory, 0, {}) + self.assertFalse(self.history.records) + self.assertIsNone(self.history.active) + + def test_best_survives_undo_and_retention_and_requires_comparable_evidence(self): + self.history.objective = {"weights": {"slack": -1}, "bounds": {"area": {"max": 20}}} + proof = self.root / "report.txt" + proof.write_text("synthetic unit-test evidence, not a real timing result") + context = {"constraints": "fixture"} + self.publish(0) + self.publish(1) + result = self.history.measure(1, {"slack": 1, "area": 10}, context, [proof]) + self.assertTrue(result["promoted"]) + best = (self.root / "best/design.v").read_bytes() + self.history.finish_undo(0) + self.publish(2) + self.assertFalse(self.history.measure(2, {"slack": 0, "area": 10}, context, [proof])["promoted"]) + self.publish(3) + self.assertFalse(self.history.measure(3, {"slack": 2, "area": 30}, context, [proof])["promoted"]) + self.history.configure(1) + self.assertEqual((self.root / "best/design.v").read_bytes(), best) + self.publish(4) + with self.assertRaises(ValueError): + self.history.measure(4, {"slack": 2, "area": 10}, {"constraints": "changed"}, [proof]) + + def test_warning_preserved_not_promoted_as_full_proof(self): + self.history.objective = {"weights": {"slack": -1}} + self.publish(0, "warning") + source = self.root / "report.txt" + source.write_text("fixture") + result = self.history.measure(0, {"slack": 3}, {"setup": "fixture"}, [source]) + self.assertFalse(result["promoted"]) + self.assertEqual(self.history.get()["export_proof"]["status"], "warning") + + def test_missing_nan_metrics_or_evidence_rejected(self): + self.publish(0) + for metrics, context, evidence in (({"slack": float("nan")}, {"setup": 1}, [__file__]), + ({"slack": 1}, {}, [__file__]), + ({"slack": 1}, {"setup": 1}, [])): + with self.assertRaises(ValueError): + self.history.measure(0, metrics, context, evidence) + + +class ScopeSelectionTests(unittest.TestCase): + def test_current_historical_undo_and_reuse(self): + current = [0] + calls, loaded = [], [] + + class Session: + libraries = [] + + @contextmanager + def use_checkpoint(self, revision=None): + key = current[0] if revision is None else revision + yield {"revision": key, "verilog_file": f"{key}.v", "top": "top", + "files": {"design.v": str(key)}, "export_proof": {"status": "proved"}} + + def call(tool, arguments): + calls.append(tool) + if tool == "load_verilog": + loaded[:] = arguments["files"] + if tool == "reset_universe": + loaded.clear() + return {"loaded": bool(loaded), "top": {"name": "top"}, "loaded_files": loaded[:], "answer": loaded[:]} + + scope = ScopeCheckpoints(Session(), call) + self.assertEqual(scope.query("get_stats")["revision"], 0) + scope.query("get_stats") + self.assertEqual(calls.count("load_verilog"), 1) + current[0] = 1 + self.assertEqual(scope.query("get_stats")["revision"], 1) + self.assertEqual(scope.query("get_stats", revision=0)["revision"], 0) + self.assertEqual(scope.query("get_stats")["revision"], 1) + current[0] = 0 + self.assertEqual(scope.query("get_stats")["result"]["answer"], ["0.v"]) + with self.assertRaises(ValueError): + scope.query("query_python") + + def test_restored_physical_metrics_must_match_all_fields(self): + baseline = {k: 1 for k in ("setup_ns", "hold_ns", "tns_ns", "area_um2", "routing_drc", "power_report")} + require_restored(baseline, dict(baseline)) + for key in baseline: + with self.assertRaises(ValueError): + require_restored(baseline, dict(baseline, **{key: 2})) + + def test_new_workflow_is_distinct_and_exercises_undo(self): + root = Path(__file__).resolve().parents[1] + old = (root / ".github/workflows/gcd-reference-verify.yml").read_text() + new = (root / ".github/workflows/gcd-undo-verify.yml").read_text() + self.assertNotIn("gcd_undo_regression.py", old) + self.assertIn("gcd_undo_regression.py", new) + self.assertIn("versioned_session_regression.py", new) + self.assertIn("if: always()", new) diff --git a/tests/test_session_startup.py b/tests/test_session_startup.py new file mode 100644 index 0000000..2cc1a61 --- /dev/null +++ b/tests/test_session_startup.py @@ -0,0 +1,60 @@ +"""Execute the documented startup contract without claiming native proof.""" + +from contextlib import redirect_stdout +import io +from pathlib import Path +import re +import unittest +from unittest.mock import patch + +from tools import live_session, versioned_session + + +ROOT = Path(__file__).resolve().parents[1] + + +class SessionStartupTests(unittest.TestCase): + def setUp(self): + document = (ROOT / "tools/live-session.md").read_text() + self.cells = re.findall(r"```python\n(.*?)\n```", document, re.DOTALL) + self.assertGreaterEqual(len(self.cells), 3) + + def test_standard_startup_selects_versioned_helper_and_edits_same_owner(self): + with patch.object(versioned_session, "VersionedDesignSession", autospec=True) as factory, \ + patch.object(live_session, "LiveDesignSession", autospec=True) as legacy: + owner = factory.return_value + proof = {"status": "proved", "proved_outputs": 1, "existing_outputs": 1} + owner.status.return_value = {"proof": proof, "netlist_revision": 0} + owner.apply_edit.return_value = proof + namespace = {} + exec(compile(self.cells[0], "tools/live-session.md:startup", "exec"), namespace) + factory.assert_called_once_with(reference="/absolute/original.v", + liberty_files=["/absolute/cells.lib"], + sessions_root="runs", retention=10) + legacy.assert_not_called() + self.assertIs(namespace["session"], owner) + self.assertIs(namespace["initial_proof"], proof) + owner.verify.assert_not_called() # Initialization already checks baseline. + script = "def edit(top):\n pass\n" + with patch.object(Path, "read_text", return_value=script), redirect_stdout(io.StringIO()): + exec(compile(self.cells[1], "tools/live-session.md:edit", "exec"), namespace) + owner.apply_edit.assert_called_once_with(script) + self.assertIs(namespace["session"], owner) + self.assertIs(namespace["result"], proof) + factory.assert_called_once() + + def test_explicit_no_export_startup_keeps_legacy_api(self): + with patch.object(live_session, "LiveDesignSession", autospec=True) as legacy, \ + patch.object(versioned_session, "VersionedDesignSession", autospec=True) as versioned: + namespace = {} + exec(compile(self.cells[2], "tools/live-session.md:no-export", "exec"), namespace) + legacy.assert_called_once_with(reference="/absolute/original.v", + liberty_files=["/absolute/cells.lib"], + work_dir="runs/my-no-export-session") + versioned.assert_not_called() + legacy.return_value.verify.assert_called_once_with() + self.assertIs(namespace["session"], legacy.return_value) + + +if __name__ == "__main__": + unittest.main() diff --git a/tools/README.md b/tools/README.md index f17ae85..b811803 100644 --- a/tools/README.md +++ b/tools/README.md @@ -62,6 +62,10 @@ Package installation accesses public registries; design files do not need to leave the machine. Configuring an external model is separate and remains the caller's choice. No Ollama service or model is installed by this repository. -For incremental editing and verification without reloading designs, see -[persistent Python/Jupyter sessions](live-session.md). Its optional kernel -dependencies are separate from the existing file-based workflow. +For helper-managed incremental editing, use `VersionedDesignSession` in +[persistent Python/Jupyter sessions](live-session.md): live SEC, automatic +verified checkpoints, retention and undo. Ordinary edits stay in memory; undo +reloads only the candidate. Kernel dependencies are separate from the existing +file-based workflow. The original no-export helper remains explicitly available. +For direct mode, use the same tool packages without a session helper; follow +the selected flow's direct skill and [revision recipe](../flow/direct-revisions.md). diff --git a/tools/kepler-formal/SKILL.md b/tools/kepler-formal/SKILL.md index d1c4950..b6253a2 100644 --- a/tools/kepler-formal/SKILL.md +++ b/tools/kepler-formal/SKILL.md @@ -8,41 +8,34 @@ description: Verify mapped designs in memory or from files with the Python-backe 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 -[persistent session](../live-session.md): automatic SEC compares the cumulative -candidate against unchanged golden in the same interpreter, without design -exports. If a candidate is later exported, separately verify the exported -representation reloaded from disk; in-memory proof cannot certify an exporter. +libraries and constraints unchanged. Keep the mode selected by the flow: + +- **Managed:** use the [session guide](../live-session.md). Its automatic live + and exported-file SEC stay mandatory, even with additional direct agent MCP + calls. Obtain the owner's attachment and refresh it after helper undo. +- **Direct:** call the file-based MCP tool below on immutable golden and the + exported candidate. No session helper, internal flow client or live attachment + is required. The agent explicitly requests each proof and records its evidence. + +Keep actual proof outcomes and coverage. In-memory proof cannot certify an +exporter, and a skill cannot automatically enforce an agent's verification calls. Live verification selects designs using native references containing `session_id`, `db_id`, `library_id`, and `design_id`, not registered aliases. Keep the returned references; never guess IDs or select by top-module name. Require the proof response and retrieved report to identify the requested pair. -Follow the [session setup](../live-session.md) to install the matching pinned -wrapper in both the owner and MCP process. File tools are unchanged. +For attached sessions only, follow the [session setup](../live-session.md) to +install the matching wrapper in both owner and MCP process. Direct file-based +mode does not need to start or attach to a live session. ## File-Based Verification -For a reviewed mapped-Verilog candidate, the [client helper](verify.py) creates -a fresh proof directory, snapshots read-only inputs, records their hashes and -package identities, calls the MCP server, and saves proof evidence: - -```sh -python tools/kepler-formal/verify.py \ - --reference /absolute/reference.v --candidate /absolute/candidate.v \ - --liberty /absolute/cells.lib --work-dir runs/candidate-01/proof -``` - -Agents may also call MCP directly. First call `get_kepler_formal_info`, then -`create_yaml_and_run_kepler_formal` with two absolute `input_paths`, absolute -`liberty_files`, and an unused, absolute `allowed_output_dir`. Set: +In direct mode, first call `get_kepler_formal_info`, then +`create_yaml_and_run_kepler_formal` through the agent's MCP connection with two +absolute `input_paths` (golden first, candidate second), absolute `liberty_files`, +and an unused, absolute `allowed_output_dir`. Use these options: ```json { @@ -60,6 +53,16 @@ Agents may also call MCP directly. First call `get_kepler_formal_info`, then } ``` +For scripted regression/command-line use, the optional [client helper](verify.py) +creates a fresh proof directory, snapshots inputs, records hashes and package +identities, calls MCP and saves evidence. Direct-mode agents need not use it: + +```sh +python tools/kepler-formal/verify.py \ + --reference /absolute/reference.v --candidate /absolute/candidate.v \ + --liberty /absolute/cells.lib --work-dir runs/candidate-01/proof +``` + Use these same assumptions for reference comparisons; record any explicit change. The file-based MCP starts a fresh Python worker, loads both designs with NajaEDA, and calls `kepler_formal.verify_designs`. There is no `verify_sec` tool in this diff --git a/tools/live-session.md b/tools/live-session.md index b8b5401..2319c62 100644 --- a/tools/live-session.md +++ b/tools/live-session.md @@ -1,13 +1,21 @@ # Persistent Python/Jupyter Sessions -Use this mode for cumulative NajaEDA edits with automatic SEC after each edit. +In **managed mode**, use `VersionedDesignSession` by default. It adds +automatic numbered Verilog checkpoints, configurable retention, undo and a +protected measured best result to the live editing helper. See +[session history](session-history.md) for retention and measurement controls. +The original `LiveDesignSession` remains an explicit +[no-export option](#explicit-no-export-mode), not the default startup path. +Direct mode does not use either helper; follow its +[revision recipe](../flow/direct-revisions.md) instead. + 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. +Ordinary edits accumulate in memory; only explicit undo reloads the candidate. +Both designs have their own database and loaded Liberty definitions; library +sharing and Naja-Scope attachment are deferred. Mandatory live SEC uses these +in-memory designs. Each saved Verilog checkpoint also gets separate file-based +SEC before publication. Scope and physical tools consume those checkpoints, +not the live objects. ## Setup @@ -32,9 +40,10 @@ The helper checks the installed Git commit, not only the package version label. When upgrading an existing MCP installation, the wrapper-only force reinstall is needed because different Git revisions can share the same version label. Reuse the installation if its commit already matches the pin. -For explicit wrapper development only, you may instead install a reviewed local -checkout with `python -m pip install --no-deps /absolute/kepler-formal-mcp` and -pass that path as `development_mcp_checkout`. This override requires installation +For explicit wrapper development in the no-export mode only, you may instead +install a reviewed local checkout with +`python -m pip install --no-deps /absolute/kepler-formal-mcp` and pass that path +as `development_mcp_checkout`. This override requires installation from that exact path and matches installed wrapper source to the checkout, recording hashes in `packages.json`. It fails if sources change after installation. Normal sessions and regressions do not need the override. @@ -57,16 +66,22 @@ Keep the same kernel and `session` object across calls. First cell: ```python -from tools.live_session import LiveDesignSession +from tools.versioned_session import VersionedDesignSession -session = LiveDesignSession( +session = VersionedDesignSession( reference="/absolute/original.v", liberty_files=["/absolute/cells.lib"], - work_dir="runs/my-live-session", # Must not already exist. + sessions_root="runs", # Creates a new session_ directory. + retention=10, ) -initial_proof = session.verify() +initial_proof = session.status()["proof"] ``` +Initialization verifies and saves baseline revision zero; no extra `verify()` +call is needed. Ten recent edited checkpoints plus baseline are retained by +default. To track a protected best result, supply an objective and record actual +tool measurements as described in [session history](session-history.md). + The model supplies a reviewed script containing `def edit(top):` and optionally pure helpers. The only design object supplied is the candidate. Its restricted API contract is defined in [edit_validation.py](edit_validation.py); unsupported @@ -87,6 +102,11 @@ print(result["status"], result["proved_outputs"], result["existing_outputs"]) `apply_edit` validates before mutation, invalidates the previous proof, edits the current candidate, and automatically runs SEC against original golden. +It then exports and verifies the saved representation before publishing a new +numbered checkpoint. Its returned result is the live proof; inspect +`session.checkpoint()["export_proof"]` for the separate saved-file proof. +If checkpointing fails, the call raises and the live edit is not automatically +undone; current-checkpoint access stays blocked until repair or undo. It does not ask a model to select the verification mode. The MCP attaches to this interpreter and calls the native Python library using explicit native references: session ID, database ID, library ID, and design ID. It resolves @@ -102,18 +122,23 @@ design IDs in the two databases cannot redirect verification. A mismatched pair in either the proof response or retrieved report is rejected. These native IDs are valid only for this live universe; they are not restart or reload handles. Do not destroy/reload designs or databases behind the -session. Close it and obtain fresh references in a new session instead. - -Inspect `session.status()` for current revision, state and proof. Closing with -`session.close()` detaches the MCP and destroys only this session's universe. +session. Use `session.undo()` for a controlled restore. It replaces the candidate +and expires the old binding; call `session.mcp_attachment()` afterward and +reattach external Kepler clients using the fresh session ID and references. + +Inspect `session.status()` for state and live proof. `revision` is the monotonic +edit-attempt counter; `netlist_revision` is the active saved design and can move +back on undo. A missing `netlist_revision` means live changes are not saved. +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. +For Scope, use `session.checkpoint()` for current or `session.checkpoint(0)` for +baseline. Load the selected Verilog and `session.libraries` in Scope's separate +MCP server, reloading only when the selection changes. The existing +`ScopeCheckpoints` adapter automates this for synchronous clients. Do not call +`export_inspection()` for normal versioned queries: the saved file already +exists. Use `session.use_checkpoint()` to pin an input during external runs. +See [selection and inspection](session-history.md#select-and-inspect). ## Outcomes And Recovery @@ -128,7 +153,10 @@ still perform no exports. Inspection of a rejected candidate is diagnostic only. A rejected script that never executes leaves the existing revision and proof intact. An execution error or counterexample does not roll back the candidate: -inspect the error and repair that same cumulative candidate through `apply_edit`. +inspect the error and repair that same cumulative candidate through `apply_edit`, +or call `undo()` to restore the last saved checkpoint. After a successful saved +edit, `undo()` restores the previous retained revision instead, deleting the +discarded checkpoint only after successful restoration and SEC. Best is protected. After a verification timeout, wait until the native call is idle and explicitly call `session.verify()` before editing again. Never treat a timeout as a warning proof. Do not forcibly destroy designs while native verification is running. @@ -136,8 +164,34 @@ proof. Do not forcibly destroy designs while native verification is running. The session hashes native connectivity, model identities and revisions before and after operations to detect untracked changes. Direct hostile Python can bypass such safeguards; use trusted dedicated kernels. A script or native -crash loses the in-memory session; automatic checkpoints/recovery are not -implemented in this first version. +crash loses the in-memory session, but already published checkpoints remain on +disk. Automatic restart/resume is not implemented. Retain saved files and proof +evidence; they are not live design handles. Do not silently replace original +golden with a saved candidate when starting a new session. + +## Explicit No-Export Mode + +Use the original helper only when no-export behavior is explicitly required, +or when maintaining existing no-export regressions. It has mandatory live SEC +but no automatic saved history, retention, best selection or undo: + +```python +from tools.live_session import LiveDesignSession + +session = LiveDesignSession( + reference="/absolute/original.v", + liberty_files=["/absolute/cells.lib"], + work_dir="runs/my-no-export-session", # Must not already exist. +) +initial_proof = session.verify() +``` + +Ordinary edits in this mode never dump or reload designs. Explicit +`export_inspection()` and `inspection_status(manifest_path)` support +[on-demand inspection](naja-scope/checkpoints.md), but do not prove exported +Verilog. Verify any exported physical-tool input separately. Repair failed edits +through `apply_edit` or start a fresh session; this mode has no `undo()`. +Existing callers keep these semantics until they explicitly switch classes. ## Evidence And Validation @@ -152,14 +206,15 @@ evidence, not proof of a later revision. Run the real packaged integration separately from offline tests: ```sh -python scripts/live_session_regression.py --work-dir runs/live-session-check +python scripts/versioned_session_regression.py --jupyter --work-dir runs/history-check ``` -It uses separate cells in one actual Jupyter kernel and the actual MCP/native -SEC: two cumulative equivalent edits, a rejected counterexample, repair, -invalid-script rejection, and stale-proof detection. No design export occurs. +It exercises actual MCP/native SEC and Scope inside a Jupyter kernel, including +checkpoints, retention, failed edits, undo, refreshed references and further edits. +The unchanged `scripts/live_session_regression.py` separately tests the original +no-export mode across notebook cells; the existing GCD workflow is unchanged. `python -m unittest discover -s tests -v` checks policy offline, not native proof. -Physical-design tools still require exported input files. An in-memory proof -alone does not certify the eventually exported file; use the existing -[file-based verifier](kepler-formal/SKILL.md) for that separate handoff. +The separate GCD undo workflow checks physical measurements against saved +checkpoints. Neither offline tests nor a small session fixture establish GCD +timing results. diff --git a/tools/live_session.py b/tools/live_session.py index 7d0c2d7..9678f2d 100644 --- a/tools/live_session.py +++ b/tools/live_session.py @@ -130,6 +130,8 @@ class LiveDesignSession: is deliberately restricted; neither Python nor the Naja native API is an OS sandbox. Verification needs no exports or reloads. Inspection copies are exported only on an explicit call, never reloaded into this kernel. + For managed agent startup, use VersionedDesignSession in versioned_session; + this base class preserves the explicit no-export API for existing callers. """ def __init__(self, reference, liberty_files, work_dir, *, timeout=600, diff --git a/tools/naja-scope/SKILL.md b/tools/naja-scope/SKILL.md index faf42ad..b0367d6 100644 --- a/tools/naja-scope/SKILL.md +++ b/tools/naja-scope/SKILL.md @@ -5,17 +5,23 @@ description: Inspect design connectivity through Naja-Scope MCP to establish dri # Inspect Before Rewiring +Keep the selected execution mode. In **managed mode**, resolve the saved file +and libraries through the [session guide](../session-history.md). In **direct +mode**, resolve them from the [revision manifest](../../flow/direct-revisions.md) +without a Python flow helper or Scope adapter. Reload Scope when that selection +changes, including after undo; reuse an unchanged loaded copy. + 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. +candidate. Load original files once for standalone baseline analysis. In the +explicit managed no-export compatibility mode only, use +[on-demand inspection](checkpoints.md): export when needed and check freshness +before using its answers. Unlike versioned mode, this compatibility mode does +not save after every edit. In both modes, reload Scope only when the next query +needs a different revision, not before every query. - Use `resolve` for exact hierarchical objects; retain underscores and bit indices. - Use `get_drivers` to identify boundary input sources. diff --git a/tools/naja-scope/checkpoints.md b/tools/naja-scope/checkpoints.md index 68a76e3..9899a19 100644 --- a/tools/naja-scope/checkpoints.md +++ b/tools/naja-scope/checkpoints.md @@ -1,5 +1,9 @@ # Inspect A Live Candidate Without Binding +This is the on-demand handoff for the explicit no-export `LiveDesignSession`. +For the default `VersionedDesignSession`, use its already saved +[numbered checkpoints](../session-history.md#select-and-inspect) instead. + 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. diff --git a/tools/najaeda/SKILL.md b/tools/najaeda/SKILL.md index 02f5323..65c4d47 100644 --- a/tools/najaeda/SKILL.md +++ b/tools/najaeda/SKILL.md @@ -5,25 +5,33 @@ description: Inspect and edit structural hardware connectivity with NajaEDA, pre # Structural Editing -Use the [package guide](install.md). For incremental edits in one Python/Jupyter -kernel, read [persistent sessions](../live-session.md). Supply only `edit(top)` -and pure helpers to `session.apply_edit(script)`; do not import, reset, load or -dump designs inside the script. The session owns loading and automatically runs -SEC against golden. Each edit starts from the previous candidate, including a -partially executed edit that needs repair after an exception. +Use the [package guide](install.md). Keep the execution mode selected by the +backend/RTL skill; this tool skill does not require a flow helper. NajaEDA is +accessed through Python in this repository, not a separate editing MCP server. -For a separate, file-based process, load Liberty before mapped Verilog: +In **managed mode**, follow [session startup](../live-session.md) and supply +only `edit(top)` and pure helpers to `session.apply_edit(script)`. Do not import, +reset, load or dump inside that restricted script. The helper owns these steps +and automatic SEC. Undo and checkpoint rules are in its session guide. + +In **direct mode**, use the Python API yourself and the +[direct revision recipe](../../flow/direct-revisions.md). Loading, editing, +exporting and requesting SEC are explicit actions; no session helper is used. + +In a fresh candidate-only process, load Liberty before mapped Verilog: ```python from najaeda import netlist -netlist.reset() netlist.load_liberty([liberty_path]) top = netlist.load_verilog([input_path]) if top is None: raise RuntimeError("No top loaded") ``` +Do not reset an existing universe holding someone else's designs. Direct mode +uses an isolated candidate process so golden remains an immutable input file. + For local gate replacements read [the boundary-preserving recipe](gate-replacement.md). Do not copy unrelated constant-source or traversal helpers into an editing script. Use the installed API and explicit pin directions; do not guess method signatures. diff --git a/tools/najaeda/gate-replacement.md b/tools/najaeda/gate-replacement.md index 3b1d9d5..6ca1002 100644 --- a/tools/najaeda/gate-replacement.md +++ b/tools/najaeda/gate-replacement.md @@ -17,9 +17,13 @@ Purpose: local structural replacement. This is not a constant-propagation helper attached. Use upper connections for child-instance pins and lower connections for top/model terminals; those are different sides of the hierarchy. 6. Delete the old instances only after every replacement is connected. If any - operation fails, discard the in-memory candidate; never export a half-edit. + operation fails in direct mode, discard that staging candidate. In managed + mode, use the owner's repair/undo operation, never reset its universe. + Never export a half-edit. Temporary overlapping drivers must not survive into an exported design. -7. Export, reload and run SEC. Preserve the input file and record the script. +7. Verify the exported design with SEC. Direct mode explicitly exports and + requests the proof; managed mode performs these steps through its helper. + Preserve the input file and record the script. Preserve every boundary output, including intermediate signals with consumers outside the replacement group. Reducing logic depth does not justify dropping diff --git a/tools/scope_checkpoints.py b/tools/scope_checkpoints.py new file mode 100644 index 0000000..ec1ef40 --- /dev/null +++ b/tools/scope_checkpoints.py @@ -0,0 +1,37 @@ +"""Select numbered checkpoints for a separate, file-based Naja-Scope MCP.""" + + +READ_ONLY = frozenset({"status", "resolve", "find", "get_hierarchy", "get_drivers", + "get_loads", "trace_cone", "get_stats", "get_module_card"}) + + +class ScopeCheckpoints: + """call(tool, arguments) is supplied by the caller's existing MCP client.""" + + def __init__(self, session, call): + self.session = session + self.call = call + self.loaded = None + + def query(self, tool, arguments=None, *, revision=None): + if tool not in READ_ONLY: + raise ValueError("Checkpoint queries must use typed read-only Scope tools") + with self.session.use_checkpoint(revision) as checkpoint: + path = checkpoint["verilog_file"] + identity = (path, checkpoint["files"]["design.v"]) + status = self.call("status", {}) + if (self.loaded != identity or not status.get("loaded") + or path not in status.get("loaded_files", [])): + self.loaded = None + self.call("reset_universe", {}) # The Scope process only. + if self.session.libraries: + self.call("load_liberty", {"files": [str(p) for p in self.session.libraries]}) + self.call("load_verilog", {"files": [path]}) + status = self.call("status", {}) + if (not status.get("loaded") or status.get("top", {}).get("name") != checkpoint["top"] + or path not in status.get("loaded_files", [])): + raise RuntimeError("Scope did not load the selected checkpoint") + self.loaded = identity + result = self.call(tool, arguments or {}) + return {"revision": checkpoint["revision"], "design_sha256": identity[1], + "result": result, "export_proof": checkpoint["export_proof"]} diff --git a/tools/session-history.md b/tools/session-history.md new file mode 100644 index 0000000..585573a --- /dev/null +++ b/tools/session-history.md @@ -0,0 +1,137 @@ +# Numbered Netlist History And Undo + +`VersionedDesignSession` is the default for managed iterative work, with saved +netlists, rollback, Scope inspection and physical measurements. Follow the +[standard startup](live-session.md) for installation and shared-kernel setup. +The original no-export `LiveDesignSession` remains an explicit compatibility mode. +All implementation is in 22b, using the existing packaged tools. +Direct mode follows the [file-based recipe](../flow/direct-revisions.md) instead +of importing this helper or its storage adapter. + +```python +from tools.versioned_session import VersionedDesignSession + +session = VersionedDesignSession( + reference="original.v", liberty_files=["cells.lib"], + sessions_root="runs", retention=10, + objective={ + "weights": {"setup_ns": -1}, # Minimize score: maximize slack. + "bounds": {"hold_ns": {"min": 0}, "routing_drc": {"max": 0}}, + }, +) +``` + +The default directory is `runs/session_/`. An explicit, +unused `work_dir` is also supported. The date identifies the session, not the +netlist revision. Numbered `versions/revision-0000/`, `revision-0001/`, etc. +contain `design.v`, a manifest, edit script where applicable, and export proof. +`inputs/` preserves original Verilog and Liberty files. Keep constraints and +physical setup immutable too; record their hashes in measurement context. + +Initialization proves the baseline and saves revision zero. Every validated +`apply_edit(script)` runs mandatory live SEC, exports the result, and runs +separate file-based SEC before publishing its checkpoint. Counterexamples and +tool errors are hard failures; partial proof remains explicitly unproven. +Incomplete checkpoint writes are never selected as current. Failed attempts +retain diagnostics, not accepted versions. If live editing succeeds but +checkpointing fails, current inspection is blocked until repair or undo. + +## Select And Inspect + +```python +current = session.checkpoint() # Latest retained, active netlist. +baseline = session.checkpoint(0) # Explicit historical selection. +session.configure_history(retention=20) +``` + +Retain ten recent edited checkpoints by default, plus the permanent baseline. +Numbers use the existing edit-attempt counter: failures can leave gaps, and undo +never reuses a number. `session.status()["revision"]` is the attempt counter; +`session.status()["netlist_revision"]` is the active saved netlist. Manifests +and file hashes are checked before reuse. + +Naja-Scope runs in a separate process. With an agent's direct MCP tools, resolve +`session.checkpoint()` (or an explicit revision), then load its Verilog and +`session.libraries` through Scope's reset/load tools if the selected copy changed. +Never reset the editing kernel. Confirm Scope's status and record the revision +with answers; current-design questions must not reuse historical data. + +For an existing synchronous MCP client, `ScopeCheckpoints(session, call)` in +[scope_checkpoints.py](scope_checkpoints.py) automates selection and refresh. +`call(tool, arguments)` returns the parsed payload and must raise on MCP errors. +`query(tool, arguments, revision=None)` defaults to current, supports historical +versions and reuses an unchanged loaded copy. It does not register an MCP with +the agent or replace the agent's own client configuration. Do not let another +writer share that Scope server during queries. + +Use `with session.use_checkpoint() as checkpoint:` around external runs. This +pins their input, prevents mid-run undo/pruning, and checks hashes afterward. +The API is for trusted local callers, not a filesystem security sandbox. + +## Undo + +```python +result = session.undo() +attachment = session.mcp_attachment() # External Kepler clients reattach here. +``` + +Undo validates the previous saved file, restores only the candidate in the same +Python kernel, and reruns SEC against unchanged golden. Only after success does +it delete the discarded latest checkpoint. Undo after an unsaved failed edit +restores the latest good checkpoint without deleting it. If intermediate versions +were pruned, undo selects the preceding retained version; baseline is permanent. + +Naja can reuse native IDs on reload. Undo expires the old Kepler attachment and +creates a new binding identity; external MCP clients must reattach and obtain +fresh references. The Python session remains alive, and golden is not reloaded. +Old proof reports remain historical. The attempt counter never decreases. +If native restoration fails, the session is marked invalid and no checkpoint is +deleted; retain the files and start a new session rather than using that candidate. + +## Measurements And Best + +```python +session.record_measurement( + {"setup_ns": 0.04, "hold_ns": 0.02, "routing_drc": 0}, + context={"constraints_sha256": "recorded-hash", "tool_version": "recorded-version"}, + evidence=["physical-run/summary.json", "physical-run/power.rpt"], +) +``` + +These values illustrate the API, not actual measurements. Supply parsed tool +results and evidence, never model estimates. The helper checks numeric validity, +required metrics, consistent context, proof policy and objective bounds; it does +not establish that arbitrary caller-provided metrics are true. Include libraries, +corners, flow, seed/thread settings and constraints in context. Each external run +needs a fresh output directory and an identified checkpoint. + +The objective minimizes the weighted sum subject to bounds. Choose units, +normalization and weights explicitly for combined goals. No objective means no +automatic best selection. Equal/worse or infeasible results do not replace best. +Promotion requires full exported SEC proof by default; `allow_unproven: True` +explicitly permits warning-labelled results without claiming full equivalence. +The general non-blocking warning policy is unchanged. + +`best/` holds an independent copy of the netlist, proof and measurements, not a +symlink into rolling history. Undo and pruning cannot delete it. Changing the +objective or physical setup requires a new comparison/session. Baseline and best +are protected independently of the rolling retention limit. + +## Validation + +The new [GCD packaged undo workflow](../.github/workflows/gcd-undo-verify.yml) +uses the same packaged tools and reference rewrite as the existing GCD workflow, +which is unchanged. It checks original/edited/restored Scope connectivity, full +SEC coverage, timing improvement, discarded-netlist deletion and best preservation. +It runs OpenROAD three times and requires restored setup, hold, TNS, area, power +report and DRC results to match this run's baseline exactly. + +```sh +python -m unittest discover -s tests -v +python scripts/versioned_session_regression.py --jupyter --work-dir runs/history-check +python scripts/gcd_undo_regression.py --work-dir runs/gcd-undo-check +``` + +Offline tests do not prove equivalence or physical results. The real history +regression also tests failed-edit recovery, Scope refresh, continued editing, +retention and rejection of stale native references after undo. diff --git a/tools/session_history.py b/tools/session_history.py new file mode 100644 index 0000000..ad38951 --- /dev/null +++ b/tools/session_history.py @@ -0,0 +1,189 @@ +"""Numbered, integrity-checked checkpoints; no native tools required here.""" + +from contextlib import contextmanager +import hashlib +import json +import math +from pathlib import Path +import shutil +import tempfile + + +def digest(path): + return hashlib.sha256(Path(path).read_bytes()).hexdigest() + + +def write_json(path, value): + path = Path(path) + data = json.dumps(value, indent=2, allow_nan=False) + "\n" + with tempfile.NamedTemporaryFile(mode="w", dir=path.parent, delete=False) as stream: + temporary = Path(stream.name) + stream.write(data) + try: + temporary.replace(path) + finally: + temporary.unlink(missing_ok=True) + + +class RevisionHistory: + def __init__(self, directory, retention=10, objective=None): + self.directory = Path(directory) + self.versions = self.directory / "versions" + self.versions.mkdir() + self.records = {} + self.active = None + self.high_water = -1 + self.leases = {} + self.best = None + self.context = None + self.objective = json.loads(json.dumps(objective)) if objective is not None else None + if self.objective is not None: + weights = self.objective.get("weights", {}) + if not weights or not all(self._number(x) for x in weights.values()): + raise ValueError("Objective requires finite numeric weights (lower score wins)") + for bounds in self.objective.get("bounds", {}).values(): + if not set(bounds) <= {"min", "max"} or not all(self._number(x) for x in bounds.values()): + raise ValueError("Objective bounds must be finite min/max values") + self.configure(retention) + + @staticmethod + def _number(value): + return type(value) in (int, float) and math.isfinite(value) + + def configure(self, retention): + if type(retention) is not int or retention < 1: + raise ValueError("Retention must be a positive integer") + self.retention = retention + write_json(self.directory / "config.json", {"retention": retention, "objective": self.objective}) + self.prune() + + def _pointer(self): + write_json(self.directory / "current.json", {"revision": self.active, + "high_water": self.high_water}) + + def publish(self, staging, revision, metadata): + if type(revision) is not int or revision <= self.high_water: + raise ValueError("Revision numbers must increase and cannot be reused") + staging = Path(staging) + if not (staging / "design.v").is_file() or not (staging / "design.v").stat().st_size: + raise ValueError("Missing checkpoint netlist") + record = dict(metadata, revision=revision, parent=self.active) + record["files"] = {str(p.relative_to(staging)): digest(p) + for p in staging.rglob("*") if p.is_file()} + write_json(staging / "manifest.json", record) + destination = self.versions / f"revision-{revision:04d}" + staging.rename(destination) + self.records[revision] = {"directory": destination, + "manifest_hash": digest(destination / "manifest.json")} + self.active = self.high_water = revision + self._pointer() + self.prune() + return self.get(revision) + + def get(self, revision=None): + revision = self.active if revision is None else revision + if type(revision) is not int or revision not in self.records: + raise ValueError("Revision is not retained in this session") + entry = self.records[revision] + directory = entry["directory"] + if digest(directory / "manifest.json") != entry["manifest_hash"]: + raise ValueError("Checkpoint manifest was modified") + record = json.loads((directory / "manifest.json").read_text()) + for name, expected in record["files"].items(): + path = directory / name + if path.is_symlink() or not path.resolve().is_relative_to(directory.resolve()) or digest(path) != expected: + raise ValueError("Checkpoint file was modified: " + name) + return dict(record, directory=str(directory), verilog_file=str(directory / "design.v")) + + @contextmanager + def acquire(self, revision=None): + record = self.get(revision) + key = record["revision"] + self.leases[key] = self.leases.get(key, 0) + 1 + try: + yield record + self.get(key) + finally: + self.leases[key] -= 1 + self.prune() + + def prune(self): + # Baseline is permanent; active tool inputs are never deleted mid-run. + recent = sorted(key for key in self.records if key != 0) + keep = set(recent[-self.retention:]) | {0, self.active} + for key in list(self.records): + if key not in keep and not self.leases.get(key): + shutil.rmtree(self.records.pop(key)["directory"]) + + def undo_target(self, discard=True): + if discard: + candidates = [key for key in self.records if key < self.active] + if not candidates: + raise ValueError("No previous checkpoint to restore") + if self.leases.get(self.active): + raise RuntimeError("Current revision is in use by another tool") + return self.get(max(candidates)) + return self.get() + + def finish_undo(self, target): + self.get(target) + discarded = [key for key in self.records if key > target] + if any(self.leases.get(key) for key in discarded): + raise RuntimeError("A discarded revision is still in use") + self.active = target + self._pointer() + for key in discarded: + shutil.rmtree(self.records.pop(key)["directory"]) + # high_water deliberately does not decrease after undo. + + def measure(self, revision, metrics, context, evidence): + record = self.get(revision) + if not metrics or not all(self._number(x) for x in metrics.values()): + raise ValueError("Measurements must be finite numeric values") + if not context or not evidence: + raise ValueError("Measurements require setup identity and evidence files") + if self.context is not None and context != self.context: + raise ValueError("Measurement setup differs from earlier results") + objective = self.objective + if objective: + required = set(objective["weights"]) | set(objective.get("bounds", {})) + if not required <= metrics.keys(): + raise ValueError("Missing objective metrics") + directory = Path(record["directory"]) / "measurements" + directory.mkdir(exist_ok=False) + for index, source in enumerate(evidence): + source = Path(source) + shutil.copyfile(source, directory / f"{index:03d}-{source.name}") + result = {"revision": revision, "design_sha256": record["files"]["design.v"], + "metrics": metrics, "context": context, "promoted": False} + self.context = json.loads(json.dumps(context)) + if objective: + score = sum(metrics[key] * weight for key, weight in objective["weights"].items()) + if not math.isfinite(score): + raise ValueError("Objective score is not finite") + eligible = record["export_proof"]["status"] == "proved" or ( + objective.get("allow_unproven", False) and record["export_proof"]["status"] == "warning") + for key, bounds in objective.get("bounds", {}).items(): + eligible &= (metrics[key] >= bounds.get("min", -math.inf) + and metrics[key] <= bounds.get("max", math.inf)) + result.update(score=score, eligible=bool(eligible)) + result["promoted"] = bool(eligible and (self.best is None or score < self.best["score"])) + write_json(directory / "result.json", result) + if result["promoted"]: + # A real copy, not a link into the rolling history. + temporary = Path(tempfile.mkdtemp(prefix=".best-", dir=self.directory)) + shutil.copytree(record["directory"], temporary, dirs_exist_ok=True) + best = self.directory / "best" + previous = self.directory / ".previous-best" + if best.exists(): + best.rename(previous) + try: + temporary.rename(best) + except BaseException: + if previous.exists(): + previous.rename(best) + raise + if previous.exists(): + shutil.rmtree(previous) + self.best = dict(result) + return result diff --git a/tools/versioned_session.py b/tools/versioned_session.py new file mode 100644 index 0000000..71ed504 --- /dev/null +++ b/tools/versioned_session.py @@ -0,0 +1,212 @@ +"""Managed agent session: live editing, numbered checkpoints and checked undo.""" + +from contextlib import contextmanager +from concurrent.futures import ThreadPoolExecutor +from datetime import datetime, timezone +import json +from pathlib import Path +import shutil +import tempfile +import threading + +from tools.live_session import LiveDesignSession, SEC, _fingerprint +from tools.session_history import RevisionHistory, digest, write_json + + +class VersionedDesignSession(LiveDesignSession): + def _record(self): + record = super()._record() + if hasattr(self, "history"): + current = getattr(self, "_checkpoint_live_hash", None) == self._candidate_hash + record.update(netlist_revision=self.history.active if current else None, + last_saved_revision=self.history.active, retention=self.history.retention, + best_revision=self.history.best["revision"] if self.history.best else None) + write_json(self.directory / "status.json", record) + return record + + def __init__(self, reference, liberty_files, work_dir=None, *, retention=10, + objective=None, sessions_root="runs", timeout=600): + self._history_lock = threading.RLock() + if work_dir is None: + root = Path(sessions_root) + root.mkdir(parents=True, exist_ok=True) + stamp = datetime.now(timezone.utc).strftime("%Y%m%dT%H%M%S.%fZ") + work_dir = root / ("session_" + stamp) + super().__init__(reference, liberty_files, work_dir, timeout=timeout) + try: + self.history = RevisionHistory(self.directory, retention, objective) + self.inputs = self.directory / "inputs" + self.inputs.mkdir() + self.reference_file = self.inputs / "golden.v" + shutil.copyfile(reference, self.reference_file) + self.reference_file.chmod(0o400) + self.libraries = [] + for i, source in enumerate(self._liberty_paths): + destination = self.inputs / f"cells-{i:03}.lib" + shutil.copyfile(source, destination) + destination.chmod(0o400) + self.libraries.append(destination) + self._input_hashes = {str(p): digest(p) for p in [self.reference_file, *self.libraries]} + if digest(self.reference_file) != self._source_hashes[str(Path(reference).resolve())]: + raise ValueError("Reference changed while starting the session") + if any(digest(dst) != self._source_hashes[str(src)] + for src, dst in zip(self._liberty_paths, self.libraries)): + raise ValueError("Library changed while starting the session") + self._undo_count = 0 + self._checkpoint_live_hash = None + self._checkpoint_epoch = 0 + super().verify() + self._checkpoint(initial=True) + except BaseException: + super().close() + raise + + def _check_inputs(self): + if any(digest(path) != sha for path, sha in self._input_hashes.items()): + raise ValueError("Session baseline or libraries were modified") + + def _file_sec(self, directory, candidate): + # Notebook cells already have an event loop. The file-based MCP client + # owns another loop; keep it off the kernel's thread, like the live client. + with ThreadPoolExecutor(max_workers=1) as executor: + return executor.submit(SEC.run_sec, directory, self.reference_file, candidate, + self.libraries, timeout=self.timeout).result() + + def _checkpoint(self, initial=False): + self._check_inputs() + staging = Path(tempfile.mkdtemp(prefix=".checkpoint-", dir=self.directory)) + try: + with self._inspection_access(): + before = self._candidate_hash + if initial: + shutil.copyfile(self.reference_file, staging / "design.v") + else: + self._candidate.dumpVerilog(str(staging), "design.v") + shutil.copyfile(self.directory / f"revision-{self.revision:04d}/edit.py", staging / "edit.py") + live_proof = json.loads(json.dumps(self.proof)) + proof = self._file_sec(staging / "export-proof", staging / "design.v") + self._check_inputs() + with self._inspection_access(): + if before != self._candidate_hash: + raise RuntimeError("Candidate changed during checkpoint verification") + record = self.history.publish(staging, self.revision, { + "top": self._candidate.getName(), "live_proof": live_proof, + "export_proof": proof, "candidate_reference": dict(self._candidate_ref), + "created_at": datetime.now(timezone.utc).isoformat(), + }) + self._checkpoint_live_hash = before + self._checkpoint_epoch += 1 + self._record() + return record + except BaseException as error: + if staging.exists(): + # Do not publish a failed/partial export as a selectable revision. + write_json(staging / "error.json", {"error": str(error)}) + raise + + def apply_edit(self, script): + with self._history_lock: + self._check_inputs() + result = super().apply_edit(script) + self._checkpoint() + return result + + def checkpoint(self, revision=None): + """Return an explicit historical version or the current saved design.""" + with self._history_lock: + with self._inspection_access(): + self._check_inputs() + if revision is None and self._checkpoint_live_hash != self._candidate_hash: + raise RuntimeError("Live candidate has unsaved changes; undo or repair it before current inspection") + return self.history.get(revision) + + @contextmanager + def use_checkpoint(self, revision=None): + """Pin the exact tool input for the duration of an external run/query.""" + with self._history_lock: + record = self.checkpoint(revision) + with self.history.acquire(record["revision"]) as leased: + yield leased + + def configure_history(self, *, retention): + with self._history_lock: + self.history.configure(retention) + + def record_measurement(self, metrics, *, context, evidence, revision=None): + with self._history_lock: + record = self.checkpoint(revision) + return self.history.measure(record["revision"], metrics, context, evidence) + + def undo(self): + """Restore first; only then delete the discarded netlist checkpoint.""" + from kepler_formal_mcp.session_bridge import SessionBridge + + with self._history_lock: + self._check_inputs() + self._undo_count += 1 + output = self.directory / f"undo-{self._undo_count:04d}" + output.mkdir() + with self._inspection_access(): + target = self.history.undo_target( + discard=self._checkpoint_live_hash == self._candidate_hash) + # Revalidate the actual persisted file before replacing any live objects. + file_proof = self._file_sec(output / "file-proof", target["verilog_file"]) + with self._operation: + self._check() + old_bridge = self._bridge + if self._pending or not old_bridge.lock.acquire(blocking=False): + raise RuntimeError("Native work is running; undo is blocked") + try: + self.history.get(target["revision"]) + self._check_inputs() + self.state, self.proof = "restoring", None + self._record() + # Naja can reuse native IDs on reload. Expire the old binding + # BEFORE destroying objects; old agent references must fail. + detached = self._client.call("close_session", {"session_id": self._session_id}) + if detached.get("status") != "success": + raise RuntimeError("Kepler could not detach before undo") + old_bridge.close() + db = self._candidate.getDB() + for library in list(db.getLibraries()): + if not library.isPrimitives(): + for design in list(library.getSNLDesigns()): + design.destroy() + db.loadVerilog([target["verilog_file"]]) + self._candidate = db.getTopDesign() + if self._candidate is None: + raise RuntimeError("Restored file did not produce a top design") + self._universe.setTopDesign(self._candidate) + self._candidate_hash = _fingerprint(self._candidate) + self._bridge = SessionBridge(output_dir=output / "formal").start() + self._golden_ref = self._bridge.design_reference(self._golden) + self._candidate_ref = self._bridge.design_reference(self._candidate) + self._check() + except BaseException: + self.state, self.proof = "invalid", None + self._record() + raise + finally: + old_bridge.lock.release() + attached = self._client.call("attach_session", { + "connection_file": str(self._bridge.connection_file)}) + write_json(output / "attachment-result.json", attached) + if attached.get("status") != "success" or attached.get("session_id") != self._bridge.session_id: + self.state, self.proof = "invalid", None + self._record() + raise RuntimeError("Kepler could not reattach after undo") + self._session_id = attached["session_id"] + proof = self._verify() + self.history.finish_undo(target["revision"]) + self._checkpoint_live_hash = self._candidate_hash + self._checkpoint_epoch += 1 + self._record() + result = {"restored_revision": target["revision"], "proof": proof, + "export_proof": file_proof, "attempt_counter": self.revision, + "reattach_required": True} + write_json(output / "result.json", result) + return result + + def close(self): + with self._history_lock: + super().close()