diff --git a/docs/README.ja.md b/docs/README.ja.md index c64ac5075..5c93e5d67 100644 --- a/docs/README.ja.md +++ b/docs/README.ja.md @@ -36,6 +36,7 @@ Harness Engineer Guide と Developer Reference の境界は **データ対コー - [形式モデルを実装に追従させる](reference/21-formal-model-following.ja.md) - [新規プロトコルへ形式モデルを供給する](reference/22-formal-model-supply.ja.md) - [Telemetry Schema reference](reference/23-telemetry-schema.ja.md) +- [Intent autonomy・レビュー・完了](reference/24-intent-autonomy.ja.md) リポジトリレイアウトの設計判断は [Workspace Layout Decision](reference/18-workspace-layout.ja.md) に記録しています。 diff --git a/docs/README.md b/docs/README.md index a72d3865d..f2d85ea41 100644 --- a/docs/README.md +++ b/docs/README.md @@ -51,6 +51,7 @@ to add one. - [Keeping a formal model in step with its implementation](reference/21-formal-model-following.md) - [Supplying a formal model for a new protocol](reference/22-formal-model-supply.md) - [Telemetry Schema reference](reference/23-telemetry-schema.md) +- [Intent autonomy, review, and completion](reference/24-intent-autonomy.md) The repository layout decision is recorded in [Workspace Layout Decision](reference/18-workspace-layout.md): the framework diff --git a/docs/guide/19-plugins.ja.md b/docs/guide/19-plugins.ja.md index be0a4f247..c0984d9af 100644 --- a/docs/guide/19-plugins.ja.md +++ b/docs/guide/19-plugins.ja.md @@ -10,8 +10,8 @@ この章は利用者向けリファレンスであり、オーサリングガイドです。プラグインシステムが 現在サポートする面、そのコマンドライン面、セッション起動時にプラグインがホストへ自動 -compose される仕組み、利用者に見える安全契約、ローカルでの検証手順、そして 7 つの -パッケージハーネス面と 5 つのセルフインストール面の違いを記述します。これはいかなる +compose される仕組み、利用者に見える安全契約、ローカルでの検証手順、そして +パッケージハーネス面とセルフインストール面の違いを記述します。これはいかなる 上流 README のコピーでもありません — 以下のパス・コマンド・失敗契約はすべて Amadeus のものです。 @@ -65,7 +65,7 @@ plugins/example/ 1. **オーサリング** — `plugins//plugin.json` と参照ファイルを書きます。 2. **投影** — パッケージャが `plugins/` を discover し、各ソースを構造的に検証 (マニフェスト存在・identity 一意・プラグイン自身のサブツリーを逸脱するパスなし) - し、各プラグインを 7 つのパッケージハーネスツリーとハーネス中立バンドルへ投影 + し、各プラグインを各パッケージハーネスツリーとハーネス中立バンドルへ投影 します。プラグインが 0 件のとき、出力はプラグイン非対応ビルドと byte-identical です。 3. **inspect** — 合成エンジンが discover 済みプラグインをホストスナップショットと @@ -120,7 +120,7 @@ verb は次のとおりです。 読み戻すルートと同一なので、install・compose・discovery が乖離することはありません。 `--project-root ` はこれを上書きして別のホストを対象にします — CLI が存在する場所 以外のホストへ compose する手段で、パッケージされるがセルフインストールされない -`kiro` / `kiro-ide` 面では常に必要です。 +`kiro` / `kiro-ide` / `pi` 面では常に必要です。 引数処理は fail-closed で、いかなる変更よりも **前** に行われます: 未知 verb・未知 フラグ・余剰引数は usage を stderr へ出して exit `2` で終わり、ホストには一切触れません。 @@ -137,8 +137,8 @@ compose を配線しています。`--if-stale` 高速路により、合成レ 起動レイテンシを増やしません。フックの失敗は stderr 警告 1 行と exit 0 であり — プラグインの問題がセッションをブロックすることはありません。 -7 つのパッケージ面すべてがこのトリガーを配線します。Kiro CLI と Kiro IDE は同じ -`.kiro` host tree を共有するため、7 面は 6 個の host directory を対象にします。 +8 つのパッケージ面すべてがこのトリガーを配線します。Kiro CLI と Kiro IDE は同じ +`.kiro` host tree を共有するため、8 面は 7 個の host directory を対象にします。 | 面 | session-start トリガー | 自動 compose | | --- | --- | --- | @@ -149,6 +149,7 @@ compose を配線しています。`--if-stale` 高速路により、合成レ | `kiro` | `agentSpawn` | 配線あり | | `kiro-ide` | `promptSubmit`(`--if-stale` で冪等) | 配線あり | | `opencode` | JavaScript plugin の `session.created` event | 配線あり | +| `pi` | extension の `session_start` event | 配線あり | OpenCode は shell hook ではなく公式 JavaScript/TypeScript plugin event を使います。既存の `.opencode/plugins/amadeus-opencode-plugin.ts` が `session.created` を処理し、`.opencode` @@ -186,7 +187,7 @@ OpenCode は shell hook ではなく公式 JavaScript/TypeScript plugin event - **`native-manifest`**(`claude`)— ホストのプラグインマーケットプレイス経由で `.claude-plugin/plugin.json` を使ってインストール。自動 compose は `hooks/hooks.json` から走ります。 -- **`folder-drop-auto`**(`codex`・`cursor`・`kimi`・`kiro`・`kiro-ide`)— バンドルの +- **`folder-drop-auto`**(`codex`・`cursor`・`kimi`・`kiro`・`kiro-ide`・`pi`)— バンドルの `plugins//` を、プロジェクトルート配下の `<ハーネスディレクトリ>/.amadeus-plugin-src//`(Codex なら `.codex/.amadeus-plugin-src//`)へコピー。ここが `compose` の走査先であり、 @@ -279,7 +280,7 @@ spec が drift したことを知らせ、*あなた* がチェック再実行 検証はローカルかつ一時的です — プラグインを試すためにコミット済みツリーを変更する ことはありません。リファレンスライフサイクルテストがモデルです。canonical ソースを 使い捨ての一時ワークスペースへコピーし、パッケージャのソース/出力ルートをそこへ -リダイレクトし(`AMADEUS_PLUGINS_ROOT` / `AMADEUS_DIST_ROOT`)、7 面すべてへ投影し、 +リダイレクトし(`AMADEUS_PLUGINS_ROOT` / `AMADEUS_DIST_ROOT`)、全面へ投影し、 一時ホストへ compose し、doctor を実行し、drop します。宣言物だけが生成・検出・除去 され、tracked tree に一時ファイルが 1 つも残らないことを assert します。 @@ -295,11 +296,50 @@ bun test tests/integration/t254-reference-plugin-lifecycle.test.ts --- -## 7 つのパッケージ面、5 つのセルフインストール面 +## import する全モジュールを宣言する -パッケージャは各プラグインを **7 つ** のハーネス面へ投影します: `claude`・`codex`・ -`cursor`・`kiro`・`kiro-ide`・`opencode`・`kimi`。セルフインストール(ハーネスを +compose されたプラグインは、`plugin.json` が宣言したファイルだけを運びます。したがって +宣言済みツールが import しているのに `tools` へ載せ忘れたヘルパーモジュールは、単なる +記載漏れではなく、compose 後の全ホストにおける import 欠落です。ファイルがディスク上に +そのまま在る自分の作業ツリーではロードでき、実際にインストールされた先で失敗します。 + +パッケージャはこれを **import-closure guard** で塞ぎます。manifest が宣言する各ツールを +起点に *相対* import(`./x.ts`・`../y.ts`)の推移閉包を辿り、到達した全モジュールが +`plugin.json` に宣言され、かつプラグイン自身のソースとして実在することを要求します。 +`node:crypto` のような bare specifier はランタイムがプラグインツリーの外から解決するため +対象外で、絶対指定は境界違反として報告されます。 + +guard は投影の一部として走るため、壊れた面を出荷する代わりにビルドが失敗します。 +allowlist も skip フラグもありません — モジュールは宣言され所有されることで通り、 +そうでなければ通りません。読めない参照は閉包から取り除かれるのではなく failure として +列挙されます。これが、import パスの typo が検査対象集合を無言で縮めることを防ぎます。 + +失敗は違反参照ごとに1行、プラグイン名を前置して出力されます。最初の1件で止まらず、 +修復すべき集合が一度に列挙されます。 + +``` +MISSING from formal-model-check plugin.json: plugins/formal-model-check/tools/helper.ts +MISSING from formal-model-check owned sources: plugins/formal-model-check/tools/helper.ts +UNREADABLE import in formal-model-check: plugins/formal-model-check/tools/typo.ts +``` + +3つの異なる修復として読みます。`MISSING from … plugin.json` は、ファイルはプラグイン内に +実在するが manifest が運んでいない — `tools` へ追加します。`MISSING from … owned sources` +は、manifest が名指すパスに対応するファイルがプラグイン内に無い状態です。 +`UNREADABLE import` は参照自体が解決できなかった場合で、ファイル不在・不正なパス・ +実体がリポジトリ外へ出る symlink のいずれかです。 + +guard の実体は `scripts/import-closure-guard.ts` にあります。内部構造とテスト配置は +[コントリビュート](../reference/11-contributing.ja.md#プラグイン-import-closure-guard) +を参照してください。 + +--- + +## 8 つのパッケージ面、5 つのセルフインストール面 + +パッケージャは各プラグインを **8 つ** のハーネス面へ投影します: `claude`・`codex`・ +`cursor`・`kiro`・`kiro-ide`・`opencode`・`kimi`・`pi`。セルフインストール(ハーネスを プロジェクトルートへ反映すること)は **閉じた 5 面** のままです: `claude`・`codex`・ -`cursor`・`opencode`・`kimi`。`kiro` と `kiro-ide` はパッケージされますがプロジェクト +`cursor`・`opencode`・`kimi`。`kiro`・`kiro-ide`・`pi` はパッケージされますがプロジェクト ルートへは決して昇格しません。2 つのマトリクスは別々の期待集合に対して検証され、一方が -他方の代替に使われることも、5 面が 7 面へ広げられることもありません。 +他方の代替に使われることも、5 面がパッケージ面の集合へ広げられることもありません。 diff --git a/docs/guide/19-plugins.md b/docs/guide/19-plugins.md index 919743691..0d5b9baa5 100644 --- a/docs/guide/19-plugins.md +++ b/docs/guide/19-plugins.md @@ -12,8 +12,8 @@ anything the workspace already owns. This chapter is the user-facing reference and the authoring guide. It describes what the plugin system supports today, its command-line surface, how a plugin is composed into a host automatically at session start, what the safety contract -guarantees, how to verify a plugin locally, and how the seven packaged harness -faces differ from the five self-install faces. It is not a copy of any upstream +guarantees, how to verify a plugin locally, and how the packaged harness +faces differ from the self-install faces. It is not a copy of any upstream README — every path, command, and failure contract below is the Amadeus one. The worked example is the reference plugin `test-pro`, kept as authoring source @@ -67,8 +67,8 @@ in-prose `rules/` paths rewritten. JSON and TypeScript are copied verbatim. 1. **Author** — write `plugins//plugin.json` and its referenced files. 2. **Project** — the packager discovers `plugins/`, validates each source structurally (a manifest is present, identities are unique, no path escapes - the plugin's own subtree), and projects every plugin into the seven packaged - harness trees plus a harness-neutral bundle. With no plugins present, the + the plugin's own subtree), and projects every plugin into each packaged + harness tree plus a harness-neutral bundle. With no plugins present, the output is byte-identical to a plugin-free build. 3. **Inspect** — the composition engine checks a discovered plugin against a host snapshot and collects *every* problem (same-name stage, malformed manifest, @@ -126,8 +126,8 @@ is installed in** — `bun .codex/tools/amadeus-plugin.ts compose` composes into `.codex/` from anywhere. That is the same root the engine reads composed plugin stages back from, so install, compose, and discovery cannot drift apart. `--project-root ` overrides it to target another host — it is how you compose -into a host that is not where the CLI lives (the `kiro` and `kiro-ide` faces, -which are packaged but never self-installed, always need it). +into a host that is not where the CLI lives (the `kiro`, `kiro-ide`, and `pi` +faces, which are packaged but never self-installed, always need it). Argument handling is fail-closed and happens **before** any mutation: an unknown verb, an unknown flag, or a surplus argument prints usage on stderr and exits `2` @@ -146,8 +146,8 @@ pays only a few `existsSync` probes and returns without recomposing, so the hook adds no startup latency in the common case. Any hook failure is a single stderr warning and a zero exit — a plugin problem never blocks the session. -All seven packaged faces wire this trigger. Kiro CLI and Kiro IDE share one -`.kiro` host tree, so the seven faces cover six host directories: +All eight packaged faces wire this trigger. Kiro CLI and Kiro IDE share one +`.kiro` host tree, so the eight faces cover seven host directories: | Face | Session-start trigger | Auto-compose | | --- | --- | --- | @@ -158,6 +158,7 @@ All seven packaged faces wire this trigger. Kiro CLI and Kiro IDE share one | `kiro` | `agentSpawn` | wired | | `kiro-ide` | `promptSubmit` (idempotent via `--if-stale`) | wired | | `opencode` | JavaScript plugin `session.created` event | wired | +| `pi` | extension `session_start` event | wired | OpenCode uses its official JavaScript/TypeScript plugin event rather than a shell hook. The existing `.opencode/plugins/amadeus-opencode-plugin.ts` handles @@ -191,13 +192,13 @@ or silently dropped — it renders as an `unknown` row that fails the check. ## Installing a plugin into a host -The packager emits a per-face **install bundle** for every one of the seven faces, +The packager emits a per-face **install bundle** for every one of the eight faces, alongside a top-level `INSTALL.md` whose steps are dispatched on the face's host class: - **`native-manifest`** (`claude`) — install through the host plugin marketplace using `.claude-plugin/plugin.json`; auto-compose runs from `hooks/hooks.json`. -- **`folder-drop-auto`** (`codex`, `cursor`, `kimi`, `kiro`, `kiro-ide`) — copy the +- **`folder-drop-auto`** (`codex`, `cursor`, `kimi`, `kiro`, `kiro-ide`, `pi`) — copy the bundle's `plugins//` into `/.amadeus-plugin-src//` under your project root (`.codex/.amadeus-plugin-src//` for Codex, and so on) — the harness-rooted directory `compose` scans, which is also the root the engine @@ -295,8 +296,8 @@ the hash matches, the advisory is silent. Verification is local and temporary — you never mutate the committed tree to try a plugin out. The reference lifecycle test is the model: it copies the canonical source into a throwaway temp workspace, redirects the packager's source and output -roots there (`AMADEUS_PLUGINS_ROOT` / `AMADEUS_DIST_ROOT`), projects into all seven -faces, composes into a temp host, runs the doctor, and drops — asserting that only +roots there (`AMADEUS_PLUGINS_ROOT` / `AMADEUS_DIST_ROOT`), projects into every +face, composes into a temp host, runs the doctor, and drops — asserting that only the declared artifacts are created, detected, and removed and that no temporary file survives in the tracked tree. @@ -312,12 +313,57 @@ clean afterwards. --- -## Seven packaged faces, five self-install faces +## Declaring every module you import -The packager projects every plugin into **seven** harness faces: `claude`, -`codex`, `cursor`, `kiro`, `kiro-ide`, `opencode`, and `kimi`. Self-install — the -reflection of a harness into the project root — stays the **closed five**: -`claude`, `codex`, `cursor`, `opencode`, and `kimi`. `kiro` and `kiro-ide` are -packaged but never promoted to the project root. The two matrices are verified -against separate expected sets; one is never used as a stand-in for the other, and -the five is never widened to seven. +A composed plugin carries exactly the files its `plugin.json` declares. So a +helper module that your declared tool imports, but that you forgot to list in +`tools`, is not a stylistic omission — it is a missing import in every composed +host. The plugin loads in your working tree, where the file is simply there on +disk, and fails wherever it is actually installed. + +The packager closes this with the **import-closure guard**. Starting from each +tool your manifest declares, it walks the transitive closure of *relative* +imports (`./x.ts`, `../y.ts`) and requires every module it reaches to be both +declared in `plugin.json` and present among your plugin's own source files. Bare +specifiers like `node:crypto` are resolved by the runtime from outside the plugin +tree and are out of scope; an absolute specifier is a boundary violation and is +reported as such. + +The guard runs as part of the projection, so a build fails rather than shipping +a broken face. It has no allowlist and no skip flag — a module passes by being +declared and owned, or not at all. A reference it cannot read is enumerated as a +failure instead of being dropped from the closure, which is what keeps a typo in +an import path from quietly shrinking the set that gets checked. + +Failures print one line per offending reference, prefixed with your plugin's +name, and the whole repair set is listed at once rather than stopping at the +first offender: + +``` +MISSING from formal-model-check plugin.json: plugins/formal-model-check/tools/helper.ts +MISSING from formal-model-check owned sources: plugins/formal-model-check/tools/helper.ts +UNREADABLE import in formal-model-check: plugins/formal-model-check/tools/typo.ts +``` + +Read them as three distinct repairs. `MISSING from … plugin.json` means the file +exists in your plugin but the manifest does not carry it — add it to `tools`. +`MISSING from … owned sources` means the manifest names a path with no file +behind it inside the plugin. `UNREADABLE import` means the reference could not be +resolved at all: an absent file, a bad path, or a symlink whose real target +leaves the repository. + +The guard lives at `scripts/import-closure-guard.ts`; its internals and test +layout are described in +[Contributing](../reference/11-contributing.md#the-plugin-import-closure-guard). + +--- + +## Eight packaged faces, five self-install faces + +The packager projects every plugin into **eight** harness faces: `claude`, +`codex`, `cursor`, `kiro`, `kiro-ide`, `opencode`, `kimi`, and `pi`. +Self-install — the reflection of a harness into the project root — stays the +**closed five**: `claude`, `codex`, `cursor`, `opencode`, and `kimi`. `kiro`, +`kiro-ide`, and `pi` are packaged but never promoted to the project root. The two +matrices are verified against separate expected sets; one is never used as a +stand-in for the other, and the five is never widened to the packaged set. diff --git a/docs/reference/11-contributing.ja.md b/docs/reference/11-contributing.ja.md index 153711e27..d3f847851 100644 --- a/docs/reference/11-contributing.ja.md +++ b/docs/reference/11-contributing.ja.md @@ -238,6 +238,29 @@ LLM 推論を必要としないハンドラ(テキストの出力、ファイル - **エージェントを列挙するドキュメントテーブル**。`docs/reference/05-agent-system.md:119-131` の Phase Participation マトリクスと、`packages/framework/core/knowledge/amadeus-shared/knowledge-readme-template.md:16-29` のエージェント→examples テーブルは手で保守されます。エージェントを追加する同じ PR で更新してください(以下のドキュメントポリシーを参照)。 - **`.claude/agents/.md` の本文コンテンツ**。パースされるのはフロントマターだけです。本文のプロース(Core Responsibilities、Knowledge Loading シーケンスなど)は、アクティブ化されたときにエージェント自身が読み取ります — 他のエージェントファイルの構造に合わせて書いてください。 +## プラグイン import-closure guard + +`scripts/import-closure-guard.ts` は、manifest 検査が構造的に見ることのできない欠陥クラスに対するパッケージャ側の答えです。manifest 検査が検証するのは `plugin.json` が**宣言した**ファイルであり、宣言済みツールから相対 import で到達可能なのに自身は未宣言、というモジュールについては何も言いません。そうしたモジュールは作業ツリーには存在し compose 後のホストには存在しないため、プラグインは書かれた場所では動き、インストールされた場所で壊れます。 + +guard は宣言済みツールを起点に相対 import の推移閉包を辿り、各メンバーが二重に被覆されていることを要求します。すなわち、composition がコピーできるよう manifest に宣言されていること、そして宣言に対応する実体があるようプラグインの所有ソースに実在することです。両方の差分は最初の1件で打ち切らず全数列挙されるため、1回のビルド失敗が修復すべき集合全体を示します。 + +**責務分割。** guard モジュールは純粋です。import specifier の POSIX 正規化とリポジトリルート境界の判断を担い、ファイルシステムへは注入された `readFile` シーム経由でのみ到達します。symlink を実体へ解決すること — 文字列正規化器には見えない escape — は具象アダプタ、すなわち `scripts/plugin-projection.ts` の `repoFileReader` の責務であり、realpath がリポジトリルートの外へ出る参照には `null` を返します。したがって不在・読取不能・escape の各参照はいずれも閉包を無言で縮めるのではなく、guard の `unreadable` 列挙へ落ちます。 + +**fail-closed。** allowlist・skip リスト・例外ハッチはありません。閉包内のモジュールは宣言され所有されることによってのみ通り、解決不能な参照は failure であって無言の省略ではありません。この性質は維持してください — ここに例外ハッチを開けることは、guard が塞ぐために存在するまさにその盲点を再び開くことです。 + +**結線。** 公開シームは `assertPluginImportClosure`(`scripts/plugin-projection.ts`)です。`scripts/package.ts` は `guardPluginClosureForCli` 経由でこれを呼び、`PluginValidationError` を診断出力と非0終了へ写して、例外が CLI から漏れる代わりにビルドが失敗するようにしています。 + +**テスト。** 2つの半分と本番結線を4ファイルが覆います。 + +```bash +bun test tests/unit/t440-import-closure-resolve.test.ts \ + tests/unit/t441-import-closure-manifest.test.ts \ + tests/integration/t442-plugin-import-closure.integration.test.ts \ + tests/integration/t443-import-closure-symlink-escape.integration.test.ts +``` + +`t440` は注入されたインメモリ FS に対して再帰走査(`resolveImportClosure`)を駆動し、`t441` は被覆検査と診断レンダリング(`checkManifestClosure`・`describeClosureFailure`)を駆動し、`t442` は `assertPluginImportClosure` を通した本番結線を assert し、`t443` は責務分割のファイルシステム側 — 純粋層には見えない symlink escape — を覆います。guard を拡張するときは対応する側を拡張してください。新しい判断は純粋モジュールへ unit テスト付きで、新しいファイルシステム escape はアダプタへ integration テスト付きで置きます。 + ## ドキュメントポリシー ファイル、ディレクトリ、コマンド、フラグを追加・削除・リネームする際: diff --git a/docs/reference/11-contributing.md b/docs/reference/11-contributing.md index 84c297647..c1b16104c 100644 --- a/docs/reference/11-contributing.md +++ b/docs/reference/11-contributing.md @@ -241,6 +241,59 @@ Agent metadata (display name, example knowledge files) is read from each agent's - **Doc tables listing agents**. The Phase Participation matrix at `docs/reference/05-agent-system.md:119-131` and the agent→examples table at `packages/framework/core/knowledge/amadeus-shared/knowledge-readme-template.md:16-29` are maintained by hand. Update them in the same PR that adds the agent (see Documentation Policy below). - **`.claude/agents/.md` body content**. Only the frontmatter is parsed. The body prose (Core Responsibilities, Knowledge Loading sequence, etc.) is read by the agent itself when activated — write it to match the other agent files' structure. +## The Plugin Import-Closure Guard + +`scripts/import-closure-guard.ts` is the packager's answer to a class of defect +the manifest checks structurally cannot see. Those checks validate the files a +`plugin.json` **declares**; they say nothing about a module that is reachable by +a relative import from a declared tool but is itself undeclared. Such a module is +present in the working tree and absent from the composed host, so the plugin +works where it was written and breaks where it is installed. + +The guard walks the transitive relative-import closure from the declared tool +entrypoints and requires each member to be covered twice: declared in the +manifest, so composition copies it, and present in the plugin's owned source +paths, so the declaration has a file behind it. Both differences are enumerated +in full rather than truncated to the first offender, so one build failure lists +the entire repair set. + +**Responsibility split.** The guard module is pure. It owns POSIX normalization +of import specifiers and the repo-root boundary judgement, and it reaches the +filesystem only through an injected `readFile` seam. Resolving symlinks to their +real target — the escape a string normalizer cannot see — belongs to the concrete +adapter, `repoFileReader` in `scripts/plugin-projection.ts`, which returns `null` +for any reference whose realpath leaves the repo root. Absent, unreadable, and +escaping references therefore all land in the guard's `unreadable` enumeration +instead of quietly shrinking the closure. + +**Fail-closed.** There is no allowlist, skip list, or exception hatch. A module +in the closure passes only by being declared and owned; an unresolvable reference +is a failure, never a silent omission. Keep it that way — an exception hatch here +reopens exactly the blind spot the guard exists to close. + +**Wiring.** `assertPluginImportClosure` (`scripts/plugin-projection.ts`) is the +public seam; `scripts/package.ts` calls it through `guardPluginClosureForCli`, +which maps a `PluginValidationError` to a printed diagnostic and a non-zero exit +so the build fails instead of letting the exception escape the CLI. + +**Tests.** Four files cover the two halves and the production wiring: + +```bash +bun test tests/unit/t440-import-closure-resolve.test.ts \ + tests/unit/t441-import-closure-manifest.test.ts \ + tests/integration/t442-plugin-import-closure.integration.test.ts \ + tests/integration/t443-import-closure-symlink-escape.integration.test.ts +``` + +`t440` drives the recursive walk (`resolveImportClosure`) against an injected +in-memory filesystem, `t441` drives the coverage check and diagnostic rendering +(`checkManifestClosure`, `describeClosureFailure`), `t442` asserts the production +wiring through `assertPluginImportClosure`, and `t443` covers the filesystem half +of the responsibility split — the symlink escape that the pure layer cannot see. +When you extend the guard, extend the matching half: a new judgement belongs in +the pure module with a unit test, a new filesystem escape belongs in the adapter +with an integration test. + ## Documentation Policy When adding, removing, or renaming files, directories, commands, or flags: diff --git a/docs/reference/12-state-machine.ja.md b/docs/reference/12-state-machine.ja.md index 38d0d8cb9..e9c8ec17b 100644 --- a/docs/reference/12-state-machine.ja.md +++ b/docs/reference/12-state-machine.ja.md @@ -265,6 +265,23 @@ session フックは発行前にアクティブな intent の `amadeus-state.md` | `DECISION_RECORDED` | `tools/amadeus-log.ts` | オプションを捕捉するため `AskUserQuestion` の前に発火 | | `QUESTION_ANSWERED` | `tools/amadeus-log.ts` | ユーザー応答の後に発火 | +#### advisory choice の受理 + +チェックポイントで hold したプラグイン advisory は、ちょうど2つの選択肢 — `run-now`(今すぐ実行する)と `defer-with-risk`(リスクを承知して延期する)— を人間へ問います。その回答の受理は `tools/amadeus-advisory-choice.ts` が所有し、意図的に狭く作られています。advisory choice が受理されるのは、実在の human turn へ結び付けられる場合だけです。 + +受理経路は2つあります。**prompt 経路**(`recordProtectedAdvisoryChoice`)はユーザーのターン本文を選択肢語彙と厳密照合します — `1`・`run-now`・日本語ラベル、`defer-with-risk` 側も同様 — それ以外は受理しません。言い換えは choice ではありません。**`record` verb** は明示経路です。 + +``` +bun .claude/tools/amadeus-advisory-choice.ts record \ + --advisory-instance --choice run-now +``` + +両経路とも receipt を `HUMAN_TURN` へ束縛します。prompt 経路は、その turn が自クローン自身の audit シャードに在ることを要求し、記録済み `HUMAN_TURN` ブロックの hash から event identity を再導出し、既に別の receipt で使用済みの turn identity を拒否します — 1つの human turn が答えるのは1つの advisory です。さらに両経路とも、対応する advisory 提示の実在を要求します。何も表示されていないターンから choice を収穫することはできません。 + +受理は **choice について冪等** です。同一 advisory instance へ同じ choice を再記録すると既存 receipt が `idempotent: true` とともに返り、既に receipt を持つ instance へ *異なる* choice を記録しようとすると、上書きではなく拒否になります。`defer-with-risk` の receipt は問いを閉じます。`run-now` の receipt が新たな choice を受け付けるのは、それが認可したモデル検査が実際にはクリーンな結果を出さなかった場合(detected・harness error・invalid)だけです。 + +`correct-misattributed` は唯一の取消経路であり、あらゆる側から囲われています。対象は `run-now` receipt に限り、それを根拠づける対応提示が存在しないときに限り、かつその試行に対するモデル検査エビデンスが存在しないときに限ります。receipt は削除されず、理由 `misattributed-unpresented-choice` とともに revoked として印されます。これらの経路はすべて audit ロック下で走ります。 + ### Scope and configuration | Event | Emitter | Notes | diff --git a/docs/reference/12-state-machine.md b/docs/reference/12-state-machine.md index f3e85253a..d8702b2a5 100644 --- a/docs/reference/12-state-machine.md +++ b/docs/reference/12-state-machine.md @@ -274,6 +274,46 @@ The canonical event set (defined in the `audit-format.md` registry) is grouped b | `DECISION_RECORDED` | `tools/amadeus-log.ts` | Fires before `AskUserQuestion` so options are captured | | `QUESTION_ANSWERED` | `tools/amadeus-log.ts` | Fires after user response | +#### Accepting an advisory choice + +A plugin advisory that holds at a checkpoint puts one question to the human with +exactly two options — `run-now` ("run it now") and `defer-with-risk` ("defer, +accepting the risk"). `tools/amadeus-advisory-choice.ts` owns the acceptance of +that answer, and it is deliberately narrow: an advisory choice is only ever +accepted when it can be tied to a real human turn. + +There are two acceptance routes. The **prompt route** +(`recordProtectedAdvisoryChoice`) matches the user's turn text against the exact +option vocabulary — `1`, `run-now`, or the Japanese label, and likewise for +`defer-with-risk` — and accepts nothing else; a paraphrase is not a choice. The +**`record` verb** is the explicit route: + +``` +bun .claude/tools/amadeus-advisory-choice.ts record \ + --advisory-instance --choice run-now +``` + +Both routes bind the receipt to a `HUMAN_TURN`. The prompt route requires the +turn to live in this clone's own audit shard, re-derives the event identity by +hashing the recorded `HUMAN_TURN` block, and refuses a turn identity that is +already spent on another receipt — one human turn answers one advisory. Both +routes further require a matching advisory presentation, so a choice cannot be +harvested from a turn where nothing was shown. + +Acceptance is **idempotent by choice**: re-recording the same choice for the +same advisory instance returns the existing receipt with `idempotent: true`, +while recording a *different* choice against an instance that already has one is +refused rather than overwriting it. A `defer-with-risk` receipt closes the +question; a `run-now` receipt admits a fresh choice only when the model check it +authorized did not actually produce a clean outcome (detected, harness error, or +invalid). + +`correct-misattributed` is the one revocation path, and it is fenced on every +side: it applies only to a `run-now` receipt, only when no matching presentation +grounds it, and only when no model-check evidence exists for that attempt. It +marks the receipt revoked with the reason `misattributed-unpresented-choice` +rather than deleting it. All of these paths run under the audit lock. + ### Scope and configuration | Event | Emitter | Notes | diff --git a/docs/reference/22-formal-model-supply.ja.md b/docs/reference/22-formal-model-supply.ja.md index 6da2c7bb7..9d643b16b 100644 --- a/docs/reference/22-formal-model-supply.ja.md +++ b/docs/reference/22-formal-model-supply.ja.md @@ -80,3 +80,46 @@ bun .claude/tools/amadeus-orchestrate.ts next --stage formal-model-check --singl ``` ステージは `run-model-check` CLI 経由で TLC を実行します。Java と `tla2tools.jar` は `formal-model-check` plugin の opt-in 依存であり、Bun-only のフレームワーク baseline には含まれません。いずれも pin されており、同じモデル・設定・image digest が同じ verdict を返します。実行面ごとの provisioning は [plugin README](../../plugins/formal-model-check/README.md) を参照してください。 + +## エビデンスを記録する: `tla-authoring` CLI + +上記ステップ6はレビュー可能なパッケージを生みます。`tla-authoring` は、そのパッケージを書き留め、アドレス付けし、後から再検査するための CLI です。あわせて、統治下の要件がモデルを伴わずに動いたことをチェックポイントへ知らせます。 + +CLI は plugin に同梱され、`plugins/formal-model-check/tools/tla-authoring.ts` に置かれ、plugin の `tools` リストへ登録されています。役割はディスパッチのみで、判断はすべて下層の `tla-evidence.ts` と `tla-applicability.ts` にあります。契約は stdout へ JSON 1行、終了コードは成功 `0`・型付き失敗 `1`・usage エラー `2` です。引数なしで実行すると、エラー経路で完全な usage を表示します。 + +``` +bun plugins/formal-model-check/tools/tla-authoring.ts +``` + +**identity(同一性)。** モデルはファイルではなく、形式化した要件テキストへ結び付きます。`identity extract` は文書を読み、閉じた文法に合致する id の節を digest します — `###` 見出し下の `FR-`・`NFR-`・`AC-` +3桁、`##` 見出し下の `ADR-` +数字です。節本文は hash 前に正準化(LF 改行・行末空白なし・前後の空行なし)されるため、散文の折り返しでは digest は動かず、ガードの変更では動きます。`identity compare` は記録済み digest に対して `current` か `stale` を報告します。 + +``` +bun plugins/formal-model-check/tools/tla-authoring.ts identity extract \ + --doc specs/tla/requirements.md --doc-kind requirements +``` + +**bundle(束)。** `bundle build` は content-addressed な envelope をエビデンスストアへ書き、`root` または先行 bundle digest である `--predecessor` へ連鎖させます。authoring bundle は applicability・trace・proof・review・approval の5レシートを、terminal-route レシートは applicability と approval だけを運びます。`bundle verify` は digest を再導出し記録済み subject identity を照合、`bundle read` はレシートを返し、`bundle list` / `bundle head` はストアと連鎖 head を列挙します。破損エントリは読み飛ばさず別枠で報告します。 + +``` +bun plugins/formal-model-check/tools/tla-authoring.ts bundle list +{"ok":true,"refs":[],"corrupted":[]} +``` + +**applicability(適用可否)。** `applicability judge` は変更申告(`{ subjects, kind, rationale }`、`kind` は `new-subject` / `semantic-change` / `impl-only` / `non-target` のいずれか)を受け取り、登録済みモデルマップに対して経路を決めます。`applicability receipt` は同じ判断を行ってレシートを構築し、参照された人間承認を、それが名指す audit シャードに対して検証します。`applicability series` は subject 集合の series key を導出します。 + +**hold(保留)。** `hold` は authoring を止めるべきかを評価します。ストアを列挙し、破損エントリが1件でもあれば解放を拒み、現在の identity と series で hold テーブルを走らせます。権威は stdout の型付き verdict であり、終了コードはそれを写すだけです。hold / no-hold を終了コードだけから読んではなりません。 + +`advisory hold` は、plugin が `requirements-analysis`・`functional-design`・`build-and-test` の各チェックポイントへ `authoring-hold` advisory として登録するラッパーです。チェックポイントは subject を知らないため、ラッパーが `specs/tla/authoring-subjects.json` から解決します。これはワークスペースが形式検証の統治下に置く文書と stable id の宣言です。何も宣言しないワークスペースは何も統治しておらず、これは抑制された no-hold ではなく真の no-hold です。一方、存在するが読めない宣言ファイルや、文書が定義しない id を名指す宣言は fail-closed します。 + +``` +bun plugins/formal-model-check/tools/tla-authoring.ts advisory hold +{"ok":true,"verdict":{"kind":"no-hold"},"reason":"no governed subjects are declared"} +``` + +## エビデンスストア + +`plugins/formal-model-check/tools/tla-evidence.ts` は CLI ではなくライブラリです。自身のエントリポイントを持たず、`tla-authoring.ts` から利用されます。エビデンスストアへの唯一の書き手であり、ストアは `--store` フラグで移さない限り `specs/tla-evidence` に置かれます。 + +ファイルは、判断側をファイルシステムなしでテストできるよう分割されています。純粋層が parse・正準化・digest・identity 比較・envelope 検証・head 解決を担い、ディスクにもクロックにもプロセスにも触れません。その下のハンドラ層がストア I/O を担い、純粋層へバイト列を渡します。書き込みは `.tmp` ディレクトリを経由して rename されるため、実行が落ちても、自分の digest だと称する名前で書きかけの bundle が残ることはありません。 + +ストアの出力を読むときに知っておく価値のある性質が2つあります。verified bundle を mint するのは `verify` だけなので、それを持っていること自体が「単に読んだ」ではなく「検査済み」の証明になります。もう1つ、走査は読めないエントリを破棄せず `corrupted` として理由(`digest-filename-mismatch` / `unparseable` / `schema-invalid`)付きで報告します。これが、破損したストアに対して hold 評価が解放を拒める根拠です。 diff --git a/docs/reference/22-formal-model-supply.md b/docs/reference/22-formal-model-supply.md index 19a6208f3..1daf05380 100644 --- a/docs/reference/22-formal-model-supply.md +++ b/docs/reference/22-formal-model-supply.md @@ -157,3 +157,98 @@ Bun-only framework baseline; both are pinned so that the same model, config, and image digest yield the same verdict. See the [plugin README](../../plugins/formal-model-check/README.md) for how each execution surface is provisioned. + +## Recording the evidence: the `tla-authoring` CLI + +Step 6 above produces a reviewable package. `tla-authoring` is how that package +is written down, addressed, and later re-checked — and how a checkpoint learns +that a governed requirement moved without its model following. + +The CLI ships with the plugin at +`plugins/formal-model-check/tools/tla-authoring.ts` and is registered in the +plugin's `tools` list. It dispatches only: every judgement lives in +`tla-evidence.ts` and `tla-applicability.ts` below it. The contract is one JSON +line on stdout, with `0` for success, `1` for a typed failure, and `2` for a +usage error. Running it with no arguments prints the full usage on the error +path: + +``` +bun plugins/formal-model-check/tools/tla-authoring.ts +``` + +**Identity.** A model is tied to the requirement text it formalises, not to a +file. `identity extract` reads a document and digests the sections whose ids +match the closed grammar — `FR-`, `NFR-`, and `AC-` followed by three digits +under a `###` heading, `ADR-` followed by digits under a `##` heading. Section +bodies are canonicalised (LF newlines, no trailing whitespace, no leading or +trailing blank lines) before hashing, so reflowing prose does not move the +digest but changing a guard does. `identity compare` reports `current` or +`stale` against a recorded digest. + +``` +bun plugins/formal-model-check/tools/tla-authoring.ts identity extract \ + --doc specs/tla/requirements.md --doc-kind requirements +``` + +**Bundles.** `bundle build` writes a content-addressed envelope into the +evidence store, chaining it to a `--predecessor` that is either `root` or an +earlier bundle digest. An authoring bundle carries five receipts — +applicability, trace, proof, review, approval; a terminal-route receipt carries +applicability and approval only. `bundle verify` re-derives the digest and +checks the recorded subject identity, `bundle read` returns the receipts, +and `bundle list` / `bundle head` enumerate the store and its chain heads, +reporting any corrupted entries separately rather than skipping them: + +``` +bun plugins/formal-model-check/tools/tla-authoring.ts bundle list +{"ok":true,"refs":[],"corrupted":[]} +``` + +**Applicability.** `applicability judge` takes a change declaration +(`{ subjects, kind, rationale }`, where `kind` is one of `new-subject`, +`semantic-change`, `impl-only`, `non-target`) and routes it against the +registered model map. `applicability receipt` performs the same judgement and +builds the receipt, verifying the referenced human approval against the audit +shard it names. `applicability series` derives the series key for a subject set. + +**The hold.** `hold` evaluates whether authoring must stop: it lists the store, +refuses to release on any corrupted entry, and runs the hold table over the +current identity and series. The typed verdict on stdout is authoritative — the +exit code only mirrors it, and no caller may read hold or no-hold from the code +alone. + +`advisory hold` is the wrapper the plugin registers as the `authoring-hold` +advisory at the `requirements-analysis`, `functional-design`, and +`build-and-test` checkpoints. A checkpoint knows no subjects, so the wrapper +resolves them from `specs/tla/authoring-subjects.json`: the documents and stable +ids a workspace places under formal-verification governance. A workspace that +declares nothing governs nothing, which is a real no-hold rather than a +suppressed one — but a declaration file that exists and cannot be read, or names +an id its documents do not define, fails closed: + +``` +bun plugins/formal-model-check/tools/tla-authoring.ts advisory hold +{"ok":true,"verdict":{"kind":"no-hold"},"reason":"no governed subjects are declared"} +``` + +## The evidence store + +`plugins/formal-model-check/tools/tla-evidence.ts` is a library, not a CLI — it +has no entry point of its own and is consumed by `tla-authoring.ts`. It is the +only writer of the evidence store, which lives at `specs/tla-evidence` unless a +`--store` flag moves it. + +The file is split so that the judgement half can be tested without a +filesystem. The pure layer owns parsing, canonicalisation, digesting, identity +comparison, envelope validation, and head resolution, and touches neither the +disk, the clock, nor the process. The handler layer below it owns store I/O and +hands the pure layer bytes. Writes stage through a `.tmp` directory and are +renamed into place, so a crashed run leaves no half-written bundle at a name +that claims to be its own digest. + +Two properties are worth knowing when reading store output. `verify` is the only +function that mints a verified bundle, so holding one is itself proof the bundle +was checked rather than merely read. And a scan reports unreadable entries as +`corrupted` — with the reason `digest-filename-mismatch`, `unparseable`, or +`schema-invalid` — instead of dropping them, which is what lets the hold +evaluation refuse to release on a damaged store. diff --git a/docs/reference/24-intent-autonomy.ja.md b/docs/reference/24-intent-autonomy.ja.md new file mode 100644 index 000000000..445b22d5f --- /dev/null +++ b/docs/reference/24-intent-autonomy.ja.md @@ -0,0 +1,172 @@ +# Intent autonomy・レビュー・完了 + +> 言語: [English](24-intent-autonomy.md) | **日本語** + +Amadeus の autonomy は1つの Intent にスコープされます。Intent はモードを持ち、 +`full` ではさらに、その Intent のためだけに人間が発行したグラントを持ちます。 +通常なら人へ問う対話へエンジンが到達したとき、モードとグラントが「自力で答えて +よいか」を決めます。答えた場合、その回答は不変の auto decision として記録され、 +人間が事後にレビューできます。 + +本章はその機構を端から端まで扱います。モードとグラント、質問の裁定方法、 +append-only なレビュー面、完了 Intent を閉じる seal、そしてこれら3つが共有する +harness registry です。監査イベントの表と各イベントの emitter は +[State Machine](12-state-machine.ja.md) を参照してください。本章はそれらの +イベントが何を意味するかを説明します。 + +## モードとグラント + +モードは3値で、Intent の autonomy projection +(`packages/framework/core/tools/amadeus-intent-autonomy.ts`)が保持します。 + +| モード | 人間なしで裁定できる範囲 | +| --- | --- | +| `none` | なし。すべてのゲートと質問が `human-required` です。 | +| `semi` | 内部ステージゲートのみ。phase boundary でないステージゲートに限り、かつモード自体が人間コマンドで設定されている場合だけです。 | +| `full` | 現在のグラントの scope が許す範囲。 | + +`none` が既定であり、legacy または読解不能な projection の着地先でもあります。 +人間由来でない2つの provenance(`system-default` と `legacy-fail-closed`)は +いずれも `none` へ解決するため、Intent が偶然 autonomy を獲得することはありません。 + +モードの設定は `amadeus-bolt.ts set-autonomy` で行います。`full` はさらに、 +表示されたグラントが実際の human turn で確認されることを要求します。まず preview し、 +表示された digest を渡し返します。 + +``` +bun .claude/tools/amadeus-bolt.ts preview-autonomy +bun .claude/tools/amadeus-bolt.ts set-autonomy --mode full \ + --confirmed-display-digest sha256:... +``` + +グラントはグローバルなスイッチではありません。Intent uuid、発行時点の scope / +norm fingerprint、対象となる対話種別(`stage-gate`・`phase-gate`・ +`walking-skeleton`・`question`)、明示的に禁止する effect 分類を持つ scope +descriptor を運びます。認可は occurrence をその scope と突き合わせます。Intent の +不一致、実行中でない workflow、scope 外の対話種別は、いずれも裁定へ落ちるのではなく +理由 `SCOPE_OUT` の `human-required` を返します。 + +effect は分類されており、5つの分類はグラントでは決して認可できません。 +`new-permission`・`irreversible`・`scope-out`・`norm-waiver`・`quality-waiver` です。 +payload が記録済み fingerprint と一致しない effect や、適用 norm fingerprint が +動いた effect は `PAYLOAD_MISMATCH` / `NORM_DRIFT` として拒否されます。したがって +autonomy は、モードにかかわらず自身の権限を広げること・品質を waive すること・ +不可逆な操作を行うことができません。 + +## 質問を裁定する + +`semi` / `full` でのゲート裁定は直接的です。根拠はモード provenance または +グラント自身であり、decider は決定的エンジンです。 + +`full` での *質問* は順序付き解決を通ります。この順序自体が要点で、より安価で +より権威ある根拠から順に参照されます。 + +1. **確認済みポリシー** — グラント発行時に人間が事前確認した回答。 + `--policies-file` から `{sourceText, selector, optionId}` として供給します。 +2. **norm** — 現在の norm fingerprint 下で selector に合致する norm fact。 + 2つの norm fact が別の選択肢を指す場合、解決は推測しません。`NORM_CONFLICT` で + workflow を park します。 +3. **history** — 同じ scope 系譜と norm fingerprint の下での、同一 selector に + 対する過去の人間裁定。 +4. **solo election** — capability が利用可能な場合。 +5. **agent recommendation** — solo election が利用不能な場合に限り、記録には + degraded capability とその理由が刻まれます。 + +いずれの分岐も、選択された option が occurrence の実提示分であること、evidence +fingerprint が実 digest であることを検証します。それ以外は裁定ではなく `invalid` +です。 + +駆動は `decide-question` verb で行い、occurrence とその文脈を JSON 文書として +渡します。 + +``` +bun .claude/tools/amadeus-bolt.ts decide-question --input question-decision.json +``` + +結果は `AutoDecisionRecord` です。decision id・occurrence id・質問と提示した +option id 群・選択された option・decider・basis kind とその fingerprint・ +principal と actor・grant id・degraded capability の有無・review state を持ちます。 +これは Intent autonomy トランザクション内で `AUTO_DECIDED` として emit され、 +トランザクションは atomic に commit されます。 + +## auto decision をレビューする + +auto decision は不変です。レビュー面(`amadeus-autonomy-review.ts` と、その本番 +audit アダプタ `amadeus-autonomy-review-production.ts`)はそれらに対する +**append-only な projection** です。レビューは裁定済み effect を再実行せず、 +グラントを変更せず、Intent を再開せず、是正 Intent も作りません。既に起きたことに +対する人間の読みを記録するだけです。 + +各 decision は review state — `not-applicable`・`unreviewed`・`accepted`・ +`flagged` — を持ちます。列挙とフィルタは次のとおりです。 + +``` +bun .claude/tools/amadeus-bolt.ts list-auto-decisions --state unreviewed +``` + +レビューの commit は2段階の確認です。人間が「何を証言しようとしているか」を正確に +見られるようにするためです。まず意図する choice を添えて detail を要求すると、面は +decision とそのコマンドの digest を返します。 + +``` +bun .claude/tools/amadeus-bolt.ts get-auto-decision --decision --choice flag \ + --classification contract-defect +``` + +続いて digest を渡し返して commit します。 + +``` +bun .claude/tools/amadeus-bolt.ts review-auto-decision --decision --choice flag \ + --classification contract-defect --confirmed-review-digest sha256:... +``` + +preview の digest と commit 時に検証される digest は同一の export 済みヘルパーで +計算されるため、表示値と検査値が drift することはありません。flag の分類は +`contract-defect`・`specification-change`・`unspecified` のいずれかです。note は +生テキストではなく digest として運ばれ、detail projection は withheld / redacted の +フィールドを無言で省略せず明示します。 + +commit は `AUTO_DECISION_REVIEWED` を append します。この経路の唯一の書き手は +本番アダプタであり、書き込みには audit ロックを取ります。 + +## completion seal + +Intent が終端状態へ達したとき、閉じるイベント群は1件ずつ append されるのでは +ありません。`amadeus-intent-completion.ts` が順序付き集合全体 — グラントが開いて +いれば `INTENT_GRANT_COMPLETED`、続いて `WORKFLOW_STATE_CLEARED`、 +`WORKFLOW_COMPLETED` — を、期待イベント identity・期待 state projection revision・ +terminal projection とともに terminal commit plan として構築します。 + +**completion seal** は、トランザクション id・完了エビデンスとその digest・ +terminal projection・result にわたる digest です。受理は厳格で、receipt は同一の +トランザクション id、期待 projection revision、そして期待どおりの順序でまったく +期待どおりのイベント identity を持たねばなりません。部分的または順序の異なる +receipt は完了ではなく `CONFLICT` です。これにより「この Intent は閉じた」は状態 +フラグではなく検査可能な主張になります。レビュー面は最後の +`INTENT_COMPLETION_TRANSACTION_COMMITTED` イベントから seal を読み、完了 Intent の +decision 群を固定された履歴に対してレビュー済みとして印付けます。 + +live なマルチハーネス検証も同じモジュールにありますが、それは **任意のエビデンス** +です。定数 `CORE_INTENT_COMPLETION_REQUIRES_LIVE_RECEIPTS` は `false` であり、本番の +workflow 完了経路は live 経路を import せず、receipt cohort を待ちもしません。 +cohort と revision は後述の registry digest を pin するため、ある registry に対して +発行された cohort を別の registry に対して replay することはできません。 + +## harness registry + +`amadeus-harness-registry.ts` は、ハーネスと各ハーネスの能力の正準テーブルです。 +Core のファイルであり、全ハーネス配布へ byte-for-byte で投影されるため、各面が +コピーを個別保守するのではなく同一の事実に同意します。 + +各 descriptor は id と表示名、2つの面フラグ — `packageFace`(パッケージャが投影 +するか)と `selfInstallFace`(プロジェクトルートへ反映しうるか)— および2つの +autonomy フラグ — `autonomyContract`(autonomy 契約を尊重するか)と +`autonomyLive`(live 検証を実行できるか)— を持ちます。`native` ブロックは、 +live 認可の供給方式(`credential-attested` または `unavailable`)、judge replay が +`invoke-once` か利用不能か、live コマンドを運ぶ環境変数(無い場合は `null`)を +記録します。 + +`PACKAGE_HARNESS_IDS` と `SELF_INSTALL_HARNESS_IDS` はこれらのフラグでテーブルを +フィルタして導出され、対応する TypeScript の union 型も同じリテラル行から導出され +ます。ハーネスの追加は1行の追加です。id の union・導出される id リスト・全消費側の +型検査がそこから従い、歩調を合わせるべき第2のリストは存在しません。 diff --git a/docs/reference/24-intent-autonomy.md b/docs/reference/24-intent-autonomy.md new file mode 100644 index 000000000..421287060 --- /dev/null +++ b/docs/reference/24-intent-autonomy.md @@ -0,0 +1,183 @@ +# Intent Autonomy, Review, and Completion + +> Languages: **English** | [日本語](24-intent-autonomy.ja.md) + +Autonomy in Amadeus is scoped to one Intent. An Intent carries a mode, and — in +`full` — a grant that a human issued for that Intent and no other. When the +engine reaches an interaction it would normally put to a person, the mode and +the grant decide whether it may answer on its own; if it does, the answer is +recorded as an immutable auto decision that a human can review afterwards. + +This chapter covers that machinery end to end: the mode table and grants, how a +question is decided, the append-only review surface, the seal that closes a +completed Intent, and the harness registry the three of them share. For the +audit-event tables and the emitter of each event, see +[State Machine](12-state-machine.md); this chapter explains what the events +mean. + +## Modes and grants + +The mode is one of three values, held on the Intent's autonomy projection +(`packages/framework/core/tools/amadeus-intent-autonomy.ts`): + +| Mode | What may be decided without a human | +| --- | --- | +| `none` | Nothing. Every gate and question is `human-required`. | +| `semi` | Internal stage gates only — a stage gate that is not a phase boundary, and only when the mode itself was set by a human command. | +| `full` | Whatever the current grant's scope allows. | + +`none` is the default, and it is also where a legacy or unreadable projection +lands: the two non-human provenances (`system-default` and +`legacy-fail-closed`) both resolve to `none`, so an Intent never acquires +autonomy by accident. + +Set the mode with `amadeus-bolt.ts set-autonomy`. `full` additionally requires +that the displayed grant be confirmed by a real human turn — preview it first, +then pass back the digest you were shown: + +``` +bun .claude/tools/amadeus-bolt.ts preview-autonomy +bun .claude/tools/amadeus-bolt.ts set-autonomy --mode full \ + --confirmed-display-digest sha256:... +``` + +A grant is not a global switch. It carries a scope descriptor naming the Intent +uuid, the scope and norm fingerprints it was issued against, the interaction +kinds it covers (`stage-gate`, `phase-gate`, `walking-skeleton`, `question`), +and the effect classifications it explicitly prohibits. Authorization compares +the occurrence against that scope: a mismatched Intent, a workflow that is not +running, or an interaction kind outside the scope all return `human-required` +with reason `SCOPE_OUT` rather than falling through to a decision. + +Effects are classified, and five classifications can never be authorized by a +grant: `new-permission`, `irreversible`, `scope-out`, `norm-waiver`, and +`quality-waiver`. An effect whose payload does not match its recorded +fingerprint, or whose applicable norm fingerprint has moved, is refused as +`PAYLOAD_MISMATCH` or `NORM_DRIFT`. Autonomy therefore cannot widen its own +permissions, waive quality, or take an irreversible action, regardless of mode. + +## Deciding a question + +A gate decision under `semi` or `full` is direct: the basis is the mode +provenance or the grant itself, and the decider is the deterministic engine. + +A *question* under `full` goes through an ordered resolution, and the order is +the point — cheaper and more authoritative bases are consulted first: + +1. **Confirmed policy** — an answer the human pre-confirmed when issuing the + grant, supplied via `--policies-file` as `{sourceText, selector, optionId}`. +2. **Norm** — an applicable norm fact matching the selector under the current + norm fingerprint. If two norm facts select different options, the resolution + does not guess: it parks the workflow with `NORM_CONFLICT`. +3. **History** — a past human ruling on the same selector under the same scope + lineage and norm fingerprint. +4. **Solo election** — when the capability is available. +5. **Agent recommendation** — only when solo election is unavailable, and the + record is stamped with the degraded capability and the reason it degraded. + +Every branch validates that the selected option is one the occurrence actually +offered and that the evidence fingerprint is a real digest; anything else is +`invalid` rather than a decision. + +Drive it with the `decide-question` verb, which takes the occurrence and its +context as a JSON document: + +``` +bun .claude/tools/amadeus-bolt.ts decide-question --input question-decision.json +``` + +The result is an `AutoDecisionRecord` — decision id, occurrence id, the question +and the option ids it offered, the selected option, the decider, the basis kind +and its fingerprint, the principal and actor, the grant id, any degraded +capability, and a review state. It is emitted as `AUTO_DECIDED` inside the +Intent autonomy transaction, which commits atomically. + +## Reviewing an auto decision + +Auto decisions are immutable. The review surface +(`amadeus-autonomy-review.ts`, with its production audit adapter +`amadeus-autonomy-review-production.ts`) is an **append-only projection** over +them: reviewing never replays the decided effect, never mutates a grant, never +reopens an Intent, and never creates a remediation Intent. It records a human's +reading of what already happened. + +Each decision carries a review state — `not-applicable`, `unreviewed`, +`accepted`, or `flagged`. List and filter them: + +``` +bun .claude/tools/amadeus-bolt.ts list-auto-decisions --state unreviewed +``` + +Committing a review is a two-step confirmation, so a human sees exactly what +they are about to attest. Ask for the detail with the choice you intend, and the +surface returns the decision together with the digest of that command: + +``` +bun .claude/tools/amadeus-bolt.ts get-auto-decision --decision --choice flag \ + --classification contract-defect +``` + +Then commit, passing the digest back: + +``` +bun .claude/tools/amadeus-bolt.ts review-auto-decision --decision --choice flag \ + --classification contract-defect --confirmed-review-digest sha256:... +``` + +The preview digest and the digest verified at commit are computed by the same +exported helper, so the value displayed and the value checked cannot drift. A +flag classification is one of `contract-defect`, `specification-change`, or +`unspecified`; notes are carried as a digest rather than raw text, and the +detail projection marks withheld or redacted fields explicitly instead of +silently omitting them. + +The commit appends `AUTO_DECISION_REVIEWED`. The production adapter is the only +writer of that path, and it takes the audit lock to do so. + +## The completion seal + +When an Intent reaches its terminal state, the closing events are not appended +one at a time. `amadeus-intent-completion.ts` builds a terminal commit plan +holding the whole ordered set — `INTENT_GRANT_COMPLETED` when a grant is open, +then `WORKFLOW_STATE_CLEARED`, then `WORKFLOW_COMPLETED` — together with the +expected event identities, the expected state projection revision, and the +terminal projection. + +The **completion seal** is a digest over the transaction id, the completion +evidence and its digest, the terminal projection, and the result. Acceptance is +strict: the receipt must carry the same transaction id, the expected projection +revision, and exactly the expected event identities in exactly the expected +order. A partial or reordered receipt is a `CONFLICT`, not a completion. This is +what makes "this Intent is closed" a checkable claim rather than a state flag — +the review surface reads the seal off the last +`INTENT_COMPLETION_TRANSACTION_COMMITTED` event to mark a completed Intent's +decisions as reviewed against a fixed history. + +Live multi-harness verification lives in the same module, but it is **optional +evidence**. The constant `CORE_INTENT_COMPLETION_REQUIRES_LIVE_RECEIPTS` is +`false`, and the production workflow completion path neither imports the live +path nor waits for a receipt cohort. Cohorts and revisions pin the registry +digest described below, so a cohort minted against one registry cannot be +replayed against another. + +## The harness registry + +`amadeus-harness-registry.ts` is the canonical table of harnesses and what each +one can do. It is a Core file projected byte-for-byte into every harness +distribution, so all faces agree on the same facts rather than each maintaining +a copy. + +Each descriptor carries an id and display name, two face flags — `packageFace` +(the packager projects into it) and `selfInstallFace` (it can be reflected into +the project root) — and two autonomy flags: `autonomyContract`, whether the +harness honours the autonomy contract, and `autonomyLive`, whether live +verification can run there. The `native` block records how the harness supplies +live authorization (`credential-attested` or `unavailable`), whether judge +replay is `invoke-once` or unavailable, and the environment variable carrying +its live command, or `null` when it has none. + +`PACKAGE_HARNESS_IDS` and `SELF_INSTALL_HARNESS_IDS` are derived from the table +by filtering on those flags, and the corresponding TypeScript union types are +derived from the same literal rows. A harness is added by adding one row: the +id unions, the derived id lists, and every consumer's type checking follow from +it, and there is no second list to keep in step.