QEDGen

トリガーとミッション

ユーザーが Solana プログラムの動作を検証したい、.qedspec を作成・レビューしたい、検証成果物を生成したい、既存の Anchor プログラムをオンボードしたい、または生成成果物を同期させたいときにこのスキルを使用します。

ミッション:

• スペックを書く前にソースコードを読みます。
• .qedspec を唯一の情報源として扱います。
• qedgen check を使用してスペックを検証します。
• qedgen codegen を使用して生成成果物をスカッフォルドします。
• 生成された Rust ハンドラー TODOs をエージェントタスクとして記入し、その後ビルドとテストを実行します。
• qedgen verify と drift gates を使用して証明とコードの同期を保ちます。

生成された Rust を完全なビジネスロジックとして提示しないでください。Anchor と Quasar の出力は実装スカッフォルドです。ハンドラーファイルは、エージェントが記入するまで、転送、イベント、CPI ワイヤリング、および非機械的な効果に対して意図的に todo!() を含むことができます。

QEDGen の実行方法

利用可能な場合はインストール済みのスキルラッパーを優先してください:

QEDGEN="$HOME/.agents/skills/qedgen/tools/qedgen"

リポジトリチェックアウトから、ローカルバイナリも機能します:

cargo run -p qedgen-solana-skills -- <command>

すべての書き込みパスは git リポジトリを想定しています。リポジトリ外でコマンドがエラーになった場合は、git init を実行するか、プロジェクトルートに移動してください。

一般的なコマンド:

$QEDGEN check --spec program.qedspec
$QEDGEN codegen --spec program.qedspec --all
$QEDGEN verify --spec program.qedspec
$QEDGEN reconcile --spec program.qedspec --code programs/ --proofs formal_verification/

リリースとリポジトリメンテナンスゲート:

bash scripts/check-version-consistency.sh
bash scripts/check-readme-drift.sh
$QEDGEN check --regen-drift

完全な CLI サーフェスとフラグについては references/cli.md を参照してください。

フロー: 検証 → スカッフォルド → 記入 → 検証

ステップ 1. プログラムを理解します。

Rust ソース、テスト、アカウントモデル、権限、PDA、トークンフロー、計算、およびライフサイクルを読みます。QEDGen プロジェクトの返却の場合は、次にコードの隣にある .qedspec を読みます。Spec.lean をソースとして扱わないでください。これは生成されます。

ステップ 2. スペックを検証します。

$QEDGEN check --spec program.qedspec --coverage
$QEDGEN check --spec program.qedspec --json

codegen または証明作業を開始する前に、.qedspec 内の lint、カバレッジ、インポート、ライフサイクル、計算、および CPI 形状の検出結果を修正します。スペックは、codegen または証明作業が始まる前に意図された動作を記述する必要があります。

ステップ 3. 生成成果物をスカッフォルドします。

$QEDGEN codegen --spec program.qedspec --target anchor --all

Quasar の場合は --target quasar を使用します。Pinocchio は予約済みで、完全なものとして約束すべきではありません。

ステップ 4. 生成された Rust を記入します。

todo!() を含む生成されたハンドラーファイルを開きます。ガード呼び出し、状態構造体、およびスペック効果を契約として使用してビジネスロジックを記入します。その後、フレームワークビルドとテストを実行して、コンパイルクリーンになるまで:

cargo check --manifest-path programs/Cargo.toml
cargo test --manifest-path programs/Cargo.toml

ステップ 5. 生成されたバックエンドを検証します。

$QEDGEN verify --spec program.qedspec --proptest
$QEDGEN verify --spec program.qedspec --kani
$QEDGEN verify --spec program.qedspec --lean

プロジェクト内に存在する成果物に関連するバックエンドのみを実行してください。このリポジトリ内の生成例については、以下も実行してください:

$QEDGEN check --regen-drift

ブラウンフィールドのオンボーディング

既存の Anchor プログラムの場合:

$QEDGEN adapt --program programs/my_program --out program.qedspec

その後、.qedspec の TODO を記入し、それを検証して、ライブプログラムと相互チェックします:

$QEDGEN check --spec program.qedspec --anchor-project programs/my_program

スペックが各ハンドラーをカバーした後、ソース drift 属性にスタンプを押します:

$QEDGEN adapt --program programs/my_program --spec program.qedspec

発行された #[qed(verified, ...)] 属性を対応するハンドラー関数の上に貼り付けます。今後のハンドラーボディ、accounts-constraint、またはスペック編集は、属性が意図的にリフレッシュされるまでビルドに失敗します。

ハンドラーディスパッチが非標準の場合は、明示的なオーバーライドを使用します:

$QEDGEN adapt --program programs/my_program --handler deposit=processor::deposit

IDL のみのオンボーディングの場合:

$QEDGEN spec --idl target/idl/my_program.json

IDL スカッフォルドは形状のみです。セマンティック保証を表現できるようにするには、ソースレビューが必要です。

Codegen の所有権

生成され、常に再生成するのは安全です:

パス	所有者	注釈
Cargo.toml	QEDGen	フレームワーク依存関係とマクロ依存関係
src/state.rs	QEDGen	アカウント/状態構造体とライフサイクルステータス
src/events.rs	QEDGen	イベント構造体
src/errors.rs	QEDGen	エラー列挙型と運用バリアント
src/guards.rs	QEDGen	要求、中止、ライフサイクル、PDA、およびトークン権限チェック
src/math.rs	QEDGen	ヘルパー計算が必要な場合にのみ発行
src/instructions/mod.rs	QEDGen	モジュール宣言と Quasar 再エクスポート
tests/kani.rs	QEDGen	Kani ハーネス
tests/proptest.rs	QEDGen	プロパティテストハーネス
src/tests.rs	QEDGen	要求時のユニットテスト
src/integration_tests.rs	QEDGen	要求時の統合テストスカッフォルド
formal_verification/Spec.lean	QEDGen	.qedspec から生成された Lean モデル

最初のスカッフォルド後のユーザー所有:

パス	所有者	注釈
src/lib.rs	ユーザーまたはエージェント	クレート外壳はカスタムインポート/モジュールを取得できます
src/instructions/<handler>.rs	ユーザーまたはエージェント	ビジネスロジックと生成された TODO がここにあります
formal_verification/Proofs.lean	ユーザーまたはエージェント	耐久性のある Lean 証明
既存プロジェクトテスト	ユーザーまたはエージェント	生成されたテストで置き換えないでください

生成されたサポートコードは、意図的なハンドラー TODO の周りでコンパイルする必要があります。サポートコードがコンパイルに失敗した場合は、ジェネレータまたは生成されたサポートを修正します。ハンドラービジネスロジックが欠落している場合は、ハンドラーを記入します。

証明のハンドオフ

テストとバウンド付きモデルチェックが不十分な場合のみ、証明エンジニアリングを使用します。

proptest を使用する場合:

• スペック反復中の高速な反例。
• ランダム化された状態遷移。
• 安い回帰チェック。

Kani を使用する場合:

• アクセス制御。
• 計算安全性。
• 保存と分離の不変式。
• バウンド付き状態機械の特性。

Lean を使用する場合:

• バウンド検索を超えたシンボリック推論が必要な DeFi 数学。
• 広い計算支払能力引数。
• 誘導的 sBPF バイトコード証明。
• Kani/proptest が十分な信頼を与えられない証明義務。

日常的な sorry 記入には Leanstral を、より難しい長時間実行される証明検索には Aristotle を使用します。証明修復の前に references/proof-patterns.md を読み、sBPF については references/sbpf.md を参照してください。

Lean を編集した後は常に lake build を実行し、証明がコンパイルされた後は qedgen check を実行して、孤立した or 欠落した義務が報告されるようにしてください。

リファレンス

必要に応じてリファレンスを読み込みます。すべてのファイルを一括読み込みしないでください。

リファレンス	使用場面
references/cli.md	完全なコマンドとフラグの詳細
references/qedspec-dsl.md	DSL 構文とモデリングパターン
references/qedspec-imports.md	import、qed.toml、qed.lock、--frozen、アップストリームチェック
references/qedspec-anchor.md	Anchor アダプターとブラウンフィールドカバレッジチェック
references/adversarial-probes.md	エージェント走査型の攻撃面チェックリスト
references/proof-patterns.md	Lean 証明タクティクスと修復パターン
references/support-library.md	Lean サポートライブラリの型と補題
references/sbpf.md	sBPF アセンブリ検証
references/kani-examples.md	スキルから移動された長い Kani ハーネス例
references/brownfield-testing.md	ブラウンフィールドプロジェクトの既存テスト戦略
references/skill-operations.md	Git 衛生、学習キャプチャ、環境、およびエラー処理
references/release-history.md	スキルから移動されたバージョン機能履歴