qedgen

分类: 开发与编程 | 上传者: QEDGen | 下载: 0 | 版本: v1.0（最新）

找到您的测试遗漏的错误。在 .qedspec 中定义 Solana 程序必须保证的内容； QEDGen 对其进行验证，生成测试和证明，并搭建代理填充 Rust 代码。当用户请求“qedgen”、“qedspec”、“验证我的代码”、“证明正确性”、形式验证、属性测试、生成的 Kani/proptest/Lean 工件或 Solana 程序正确性时触发。

更新日志: Source: GitHub https://github.com/QEDGen/solana-skills

目录结构

当前层级: tree/main/

📁 .github/
- 📁 ISSUE_TEMPLATE/
  - 📄 qedspec-bug.yml 5.3 KB
- 📁 workflows/
  - 📄 ci.yml 1.5 KB
  - 📄 lake-build.yml 2.4 KB
  - 📄 release.yml 1.9 KB
📁 crates/
- 📁 qedgen/
  - 📁 src/
    
    📄 anchor_adapt.rs 62.6 KB
    
    📄 anchor_check.rs 18.3 KB
    
    📄 anchor_project.rs 10.8 KB
    
    📄 anchor_resolver.rs 41.3 KB
    
    📄 api.rs 25.9 KB
    
    📄 aristotle.rs 15.3 KB
    
    📄 asm2lean.rs 30.0 KB
    
    📄 ast.rs 26.9 KB
    
    📄 banner.rs 824 B
    
    📄 check.rs 244.7 KB
    
    📄 chumsky_adapter.rs 121.8 KB
    
    📄 chumsky_parser.rs 112.3 KB
    
    📄 codegen.rs 149.9 KB
    
    📄 consolidate.rs 6.1 KB
    
    📄 deps.rs 5.0 KB
    
    📄 drift.rs 38.6 KB
    
    📄 fill.rs 18.3 KB
    
    📄 fingerprint.rs 11.3 KB
    
    📄 idl.rs 7.0 KB
    
    📄 idl2spec.rs 28.6 KB
    
    📄 import_resolver.rs 39.9 KB
    
    📄 init.rs 23.7 KB
    
    📄 integration_test.rs 25.1 KB
    
    📄 interface_gen.rs 7.9 KB
    
    📄 kani.rs 47.6 KB
    
    📄 lean_gen.rs 208.9 KB
    
    📄 main.rs 75.7 KB
    
    📄 probe.rs 61.7 KB
    
    📄 project.rs 5.0 KB
    
    📄 proofs_bootstrap.rs 7.3 KB
    
    📄 proptest_gen.rs 52.5 KB
    
    📄 qed_lock.rs 23.1 KB
    
    📄 qed_manifest.rs 11.0 KB
    
    📄 ratchet.rs 18.9 KB
    
    📄 reconcile.rs 26.1 KB
    
    📄 regen_drift.rs 17.6 KB
    
    📄 rust_codegen_util.rs 38.8 KB
    
    📄 sbpf_verify.rs 2.9 KB
    
    📄 spec_hash.rs 29.4 KB
    
    📄 unit_test.rs 29.8 KB
    
    📄 upstream_check.rs 16.8 KB
    
    📄 validate.rs 6.2 KB
    
    📄 verify.rs 13.6 KB
  - 📁 templates/
    
    📄 .gitignore 67 B
    
    📄 integration-helpers-base.rs 316 B
    
    📄 integration-helpers-token.rs 701 B
    
    📄 lakefile.lean 198 B
    
    📄 lean-toolchain 28 B
    
    📄 Main.lean 154 B
    
    📄 program-Cargo.toml 1.4 KB
    
    📄 PROMPT_TEMPLATE.md 3.2 KB
    
    📄 README.lean.md 1.6 KB
  - 📁 tests/
    
    📄 codegen_smoke.rs 6.9 KB
    
    📄 example_manifests.rs 1.4 KB
  - 📄 Cargo.toml 1.6 KB
- 📁 qedgen-macros/
  - 📁 src/
    
    📄 lib.rs 2.3 KB
    
    📄 spec_bind.rs 31.3 KB
    
    📄 verified.rs 14.9 KB
  - 📄 Cargo.toml 347 B
📁 docs/
- 📁 design/
  - 📄 spec-composition.md 18.1 KB
- 📁 prds/
  - 📄 RELEASE-v2.10.md 11.0 KB
  - 📄 RELEASE-v2.11.2.md 6.9 KB
  - 📄 RELEASE-v2.11.3.md 8.7 KB
  - 📄 RELEASE-v2.11.4.md 5.0 KB
  - 📄 RELEASE-v2.11.md 11.4 KB
  - 📄 RELEASE-v2.15.md 6.3 KB
  - 📄 RELEASE-v2.8.md 5.9 KB
  - 📄 RELEASE-v2.9.md 16.3 KB
- 📄 CNAME 10 B
- 📄 index.html 7.8 KB
- 📄 llms-full.txt 14.1 KB
- 📄 llms.txt 4.1 KB
- 📄 logo-dark.png 15.1 KB
- 📄 logo-dark.svg 648 B
- 📄 logo-light.png 15.1 KB
- 📄 logo-light.svg 648 B
- 📄 logo.png 149.5 KB
- 📄 og.html 7.2 KB
- 📄 og.png 52.5 KB
- 📄 qgn_demo.html 69.3 KB
- 📄 style.css 11.3 KB
- 📄 verilog-lessons.md 8.5 KB
📁 examples/
- 📁 anchor-brownfield-demo/
  - 📁 src/
    
    📁 instructions/
    
    📄 increment.rs 385 B
    
    📄 initialize.rs 273 B
    
    📄 mod.rs 39 B
    
    📄 lib.rs 1.4 KB
  - 📄 after.qedspec 1008 B
  - 📄 before.qedspec 983 B
  - 📄 README.md 2.2 KB
- 📁 qed-drift-fixture/
  - 📁 src/
    
    📄 lib.rs 4.3 KB
  - 📄 Cargo.toml 514 B
  - 📄 example.qedspec 1.1 KB
  - 📄 README.md 2.1 KB
- 📁 quasar-readiness/
  - 📄 escrow.json 2.3 KB
  - 📄 escrow.v2.json 2.0 KB
  - 📄 README.md 2.8 KB
- 📁 regressions/
  - 📁 anchor-accounts-collision/
    
    📁 src/
    
    📁 a/
    
    📄 mod.rs 141 B
    
    📁 b/
    
    📄 mod.rs 264 B
    
    📄 lib.rs 1.4 KB
    
    📄 collision.qedspec 506 B
    
    📄 README.md 2.1 KB
  - 📁 anchor-adapter-shapes/
    
    📁 marinade-style/
    
    📁 src/
    
    📁 instructions/
    
    📄 deposit.rs 411 B
    
    📄 liquid_unstake.rs 349 B
    
    📄 mod.rs 41 B
    
    📄 lib.rs 1.4 KB
    
    📄 before.qedspec 1005 B
    
    📄 README.md 1.5 KB
    
    📁 squads-style/
    
    📁 src/
    
    📄 lib.rs 1.8 KB
    
    📄 before.qedspec 1014 B
    
    📄 README.md 1.4 KB
  - 📁 anchor-forwarder-multistmt/
    
    📁 src/
    
    📁 instructions/
    
    📄 buy.rs 158 B
    
    📄 fence.rs 116 B
    
    📄 mod.rs 44 B
    
    📄 settle.rs 138 B
    
    📄 lib.rs 1.9 KB
    
    📄 README.md 2.3 KB
  - 📁 const-resolution/
    
    📄 repro-check-const-counterexample.qedspec 981 B
    
    📄 repro-lean-const-witness.qedspec 857 B
    
    📄 repro-proptest-small-bound.qedspec 985 B
  - 📁 issue-8/
    
    📄 pool.qedspec 36.0 KB
    
    📄 README.md 3.6 KB
    
    📄 repro-01-u16-type.qedspec 673 B
    
    📄 repro-02-composite-or-parens.qedspec 1.1 KB
    
    📄 repro-03-duplicate-theorem.qedspec 1.0 KB
    
    📄 repro-04-liveness-params.qedspec 1.1 KB
    
    📄 repro-05-uninterpreted-helper.qedspec 1.2 KB
    
    📄 repro-06-cover-witness-bool.qedspec 1.3 KB
    
    📄 repro-07-const-pubkey-assign.qedspec 989 B
    
    📄 repro-07-pubkey-literal-assign.qedspec 1.4 KB
    
    📄 repro-08-const-pubkey-compare.qedspec 1.0 KB
    
    📄 repro-08-pubkey-literal-compare.qedspec 736 B
  - 📁 pda-collision/
    
    📄 repro-pda-seed-collision.qedspec 204 B
    
    📄 repro-pda-seed-possible-collision.qedspec 253 B
  - 📁 quantifiers/
    
    📄 repro-forall-u64.qedspec 943 B
    
    📄 repro-forall-u8.qedspec 856 B
    
    📄 repro-forall-value-binder.qedspec 1.1 KB
- 📁 rust/
  - 📁 escrow/
    
    📁 .github/
    
    📁 workflows/
    
    📄 verify.yml 912 B
    
    📁 .qed/
    
    📄 .gitignore 51 B
    
    📄 config.json 94 B
    
    📁 formal_verification/
    
    📄 .gitignore 87 B
    
    📄 lake-manifest.json 340 B
    
    📄 lakefile.lean 178 B
    
    📄 lean-toolchain 28 B
    
    📄 Proofs.lean 561 B
    
    📄 README.md 662 B
    
    📄 Spec.lean 8.7 KB
    
    📄 VERIFICATION_SCOPE.md 5.2 KB
    
    📁 migrations/
    
    📄 deploy.ts 428 B
    
    📁 programs/
    
    📁 escrow/
    
    📁 src/
    
    📄 lib.rs 7.7 KB
    
    📄 Cargo.lock 74.8 KB
    
    📄 Cargo.toml 376 B
    
    📄 Xargo.toml 62 B
    
    📁 src/
    
    📁 instructions/
    
    📄 cancel.rs 1.8 KB
    
    📄 exchange.rs 2.2 KB
    
    📄 initialize.rs 1.9 KB
    
    📄 mod.rs 242 B
    
    📄 errors.rs 286 B
    
    📄 events.rs 441 B
    
    📄 guards.rs 3.3 KB
    
    📄 lib.rs 970 B
    
    📄 state.rs 581 B
    
    📄 Cargo.lock 14.3 KB
    
    📄 Cargo.toml 379 B
    
    📁 src/
    
    📁 instructions/
    
    📄 cancel.rs 909 B
    
    📄 exchange.rs 956 B
    
    📄 initialize.rs 1.1 KB
    
    📄 mod.rs 242 B
    
    📄 errors.rs 286 B
    
    📄 events.rs 441 B
    
    📄 guards.rs 3.3 KB
    
    📄 integration_tests.rs 11.6 KB
    
    📄 lib.rs 1.0 KB
    
    📄 state.rs 581 B
    
    📄 tests.rs 6.5 KB
    
    📁 tests/
    
    📄 escrow.ts 8.6 KB
    
    📄 kani.rs 6.3 KB
    
    📄 proptest.rs 2.9 KB
    
    📄 .gitignore 67 B
    
    📄 .prettierignore 61 B
    
    📄 Anchor.toml 353 B
    
    📄 Cargo.lock 11.9 KB
    
    📄 Cargo.toml 379 B
    
    📄 escrow.qedspec 3.7 KB
    
    📄 package.json 528 B
    
    📄 qed.toml 223 B
    
    📄 tsconfig.json 205 B
  - 📁 escrow-split/
    
    📁 .qed/
    
    📄 .gitignore 51 B
    
    📄 config.json 87 B
    
    📁 formal_verification/
    
    📁 lean_solana/
    
    📁 QEDGen/
    
    📁 Solana/
    
    📄 Account.lean 5.3 KB
    
    📄 CommandBuilders.lean 7.6 KB
    
    📄 Cpi.lean 9.7 KB
    
    📄 Spec.lean 27.7 KB
    
    📄 State.lean 1.9 KB
    
    📄 Valid.lean 1.7 KB
    
    📄 Solana.lean 134 B
    
    📄 lakefile.lean 505 B
    
    📄 lean-toolchain 28 B
    
    📄 QEDGen.lean 216 B
    
    📄 .gitignore 67 B
    
    📄 lake-manifest.json 336 B
    
    📄 lakefile.lean 180 B
    
    📄 lean-toolchain 28 B
    
    📄 Proofs.lean 561 B
    
    📄 Spec.lean 5.2 KB
    
    📁 handlers/
    
    📄 cancel.qedspec 559 B
    
    📄 exchange.qedspec 723 B
    
    📄 initialize.qedspec 835 B
    
    📄 escrow.qedspec 1.1 KB
    
    📄 properties.qedspec 264 B
    
    📄 qed.lock 387 B
    
    📄 qed.toml 478 B
  - 📁 lending/
    
    📁 .github/
    
    📁 workflows/
    
    📄 verify.yml 912 B
    
    📁 .qed/
    
    📄 .gitignore 51 B
    
    📄 config.json 96 B
    
    📁 formal_verification/
    
    📄 lake-manifest.json 341 B
    
    📄 lakefile.lean 171 B
    
    📄 lean-toolchain 28 B
    
    📄 Proofs.lean 977 B
    
    📄 Spec.lean 12.2 KB
    
    📁 programs/
    
    📁 src/
    
    📁 instructions/
    
    📄 borrow.rs 2.0 KB
    
    📄 deposit.rs 1.5 KB
    
    📄 init_pool.rs 1.3 KB
    
    📄 liquidate.rs 1.8 KB
    
    📄 mod.rs 321 B
    
    📄 repay.rs 1.6 KB
    
    📄 errors.rs 396 B
    
    📄 events.rs 650 B
    
    📄 guards.rs 5.5 KB
    
    📄 lib.rs 1.2 KB
    
    📄 state.rs 844 B
    
    📄 Cargo.lock 14.3 KB
    
    📄 Cargo.toml 380 B
    
    📁 tests/
    
    📄 kani.rs 14.3 KB
    
    📄 proptest.rs 9.6 KB
    
    📄 lending.qedspec 5.0 KB
    
    📄 qed.toml 224 B
  - 📁 multisig/
    
    📁 .github/
    
    📁 workflows/
    
    📄 verify.yml 912 B
    
    📁 .qed/
    
    📄 .gitignore 51 B
    
    📄 config.json 98 B
    
    📁 formal_verification/
    
    📄 lake-manifest.json 3.5 KB
    
    📄 lakefile.lean 424 B
    
    📄 lean-toolchain 28 B
    
    📄 Proofs.lean 5.9 KB
    
    📄 Spec.lean 4.2 KB
    
    📁 programs/
    
    📁 src/
    
    📁 instructions/
    
    📄 add_member.rs 1.1 KB
    
    📄 approve.rs 1.3 KB
    
    📄 cancel_proposal.rs 1.1 KB
    
    📄 create_vault.rs 1.5 KB
    
    📄 execute.rs 1.1 KB
    
    📄 mod.rs 507 B
    
    📄 propose.rs 1.1 KB
    
    📄 reject.rs 1.3 KB
    
    📄 remove_member.rs 1.1 KB
    
    📄 errors.rs 389 B
    
    📄 events.rs 763 B
    
    📄 guards.rs 7.7 KB
    
    📄 lib.rs 1.8 KB
    
    📄 state.rs 582 B
    
    📄 Cargo.lock 14.0 KB
    
    📄 Cargo.toml 346 B
    
    📁 tests/
    
    📄 kani.rs 40.2 KB
    
    📄 proptest.rs 20.2 KB
    
    📄 multisig.qedspec 7.4 KB
    
    📄 qed.toml 225 B
  - 📁 percolator/
    
    📁 .cargo/
    
    📄 config.toml 33 B
    
    📁 .github/
    
    📁 workflows/
    
    📄 verify.yml 912 B
    
    📁 .qed/
    
    📄 .gitignore 51 B
    
    📄 config.json 102 B
    
    📁 examples/
    
    📄 offsets.rs 1.3 KB
    
    📁 formal_verification/
    
    📄 lake-manifest.json 3.5 KB
    
    📄 lakefile.lean 277 B
    
    📄 lean-toolchain 28 B
    
    📄 Proofs.lean 12.9 KB
    
    📄 Spec.lean 9.1 KB
    
    📁 programs/
    
    📁 src/
    
    📁 instructions/
    
    📄 add_lp.rs 997 B
    
    📄 add_user.rs 1005 B
    
    📄 close_account.rs 1.2 KB
    
    📄 complete_drain.rs 929 B
    
    📄 convert_released_pnl.rs 1.2 KB
    
    📄 deposit.rs 1.2 KB
    
    📄 deposit_fee_credits.rs 1.3 KB
    
    📄 execute_trade.rs 1002 B
    
    📄 liquidate_case_0.rs 941 B
    
    📄 liquidate_case_1.rs 1004 B
    
    📄 liquidate_otherwise.rs 952 B
    
    📄 mod.rs 1.1 KB
    
    📄 reclaim_empty_account.rs 1.0 KB
    
    📄 reset.rs 895 B
    
    📄 settle_account.rs 942 B
    
    📄 top_up_insurance.rs 1.1 KB
    
    📄 trigger_adl.rs 917 B
    
    📄 withdraw.rs 1.2 KB
    
    📄 errors.rs 400 B
    
    📄 guards.rs 14.1 KB
    
    📄 lib.rs 3.4 KB
    
    📄 math.rs 825 B
    
    📄 state.rs 671 B
    
    📄 Cargo.lock 14.0 KB
    
    📄 Cargo.toml 348 B
    
    📁 scripts/
    
    📄 audit-proof-strength.md 6.4 KB
    
    📄 proof-strength-audit-results.md 89.2 KB
    
    📄 run_kani_full_audit.sh 1.2 KB
    
    📁 src/
    
    📄 i128.rs 20.4 KB
    
    📄 percolator.rs 139.3 KB
    
    📄 wide_math.rs 59.8 KB
    
    📁 tests/
    
    📁 common/
    
    📄 mod.rs 4.7 KB
    
    📄 amm_tests.rs 7.4 KB
    
    📄 fuzzing.proptest-regressions 4.7 KB
    
    📄 fuzzing.rs 43.1 KB
    
    📄 kani.rs 59.1 KB
    
    📄 proofs_arithmetic.rs 17.1 KB
    
    📄 proofs_audit.rs 35.0 KB
    
    📄 proofs_instructions.rs 64.8 KB
    
    📄 proofs_invariants.rs 21.0 KB
    
    📄 proofs_lazy_ak.rs 22.4 KB
    
    📄 proofs_liveness.rs 17.1 KB
    
    📄 proofs_safety.rs 104.2 KB
    
    📄 proofs_v1131.rs 25.4 KB
    
    📄 proptest.rs 48.2 KB
    
    📄 unit_tests.rs 93.8 KB
    
    📄 .gitignore 320 B
    
    📄 Cargo.lock 8.5 KB
    
    📄 Cargo.toml 639 B
    
    📄 LICENSE 11.1 KB
    
    📄 percolator.qedspec 8.9 KB
    
    📄 qed.toml 227 B
    
    📄 README.md 4.9 KB
    
    📄 spec.md 108.4 KB
- 📁 sbpf/
  - 📁 counter/
    
    📁 .qed/
    
    📄 .gitignore 51 B
    
    📄 config.json 96 B
    
    📁 formal_verification/
    
    📄 lake-manifest.json 341 B
    
    📄 lakefile.lean 222 B
    
    📄 lean-toolchain 28 B
    
    📄 Program.lean 22.0 KB
    
    📄 Spec.lean 3.6 KB
    
    📁 src/
    
    📄 counter.s 22.9 KB
    
    📄 counter.qedspec 2.2 KB
  - 📁 dropset/
    
    📁 .qed/
    
    📄 .gitignore 51 B
    
    📄 config.json 96 B
    
    📁 formal_verification/
    
    📄 lake-manifest.json 341 B
    
    📄 lakefile.lean 222 B
    
    📄 lean-toolchain 29 B
    
    📄 Program.lean 60.9 KB
    
    📄 Spec.lean 81.7 KB
    
    📁 src/
    
    📄 dropset.s 29.3 KB
    
    📄 dropset.qedspec 4.2 KB
  - 📁 slippage/
    
    📁 .qed/
    
    📄 .gitignore 51 B
    
    📄 config.json 98 B
    
    📁 formal_verification/
    
    📄 lake-manifest.json 342 B
    
    📄 lakefile.lean 225 B
    
    📄 lean-toolchain 28 B
    
    📄 Program.lean 1.3 KB
    
    📄 Spec.lean 1.7 KB
    
    📁 src/
    
    📁 asm-slippage/
    
    📄 asm-slippage.s 698 B
    
    📄 slippage.qedspec 1.0 KB
  - 📁 transfer/
    
    📁 .qed/
    
    📄 .gitignore 51 B
    
    📄 config.json 98 B
    
    📁 formal_verification/
    
    📄 lake-manifest.json 342 B
    
    📄 lakefile.lean 225 B
    
    📄 lean-toolchain 28 B
    
    📄 Program.lean 4.7 KB
    
    📄 Spec.lean 4.3 KB
    
    📁 src/
    
    📄 transfer.s 2.4 KB
    
    📄 transfer.qedspec 1.8 KB
  - 📁 tree/
    
    📁 .qed/
    
    📄 .gitignore 51 B
    
    📄 config.json 90 B
    
    📁 formal_verification/
    
    📄 lake-manifest.json 338 B
    
    📄 lakefile.lean 213 B
    
    📄 lean-toolchain 28 B
    
    📄 Program.lean 120.9 KB
    
    📄 Spec.lean 4.1 KB
    
    📁 src/
    
    📄 tree.s 61.1 KB
    
    📄 tree.qedspec 3.9 KB
📁 interfaces/
- 📄 spl_token.qedspec 3.3 KB
📁 lean_solana/
- 📁 QEDGen/
  - 📁 Solana/
    
    📁 SBPF/
    
    📄 Execute.lean 22.9 KB
    
    📄 ISA.lean 5.1 KB
    
    📄 Memory.lean 12.0 KB
    
    📄 Patterns.lean 26.0 KB
    
    📄 Pubkey.lean 3.6 KB
    
    📄 Region.lean 5.5 KB
    
    📄 Tactic.lean 638 B
    
    📄 WPTactic.lean 5.9 KB
    
    📄 Account.lean 5.3 KB
    
    📄 Arithmetic.lean 7.0 KB
    
    📄 Bridge.lean 10.8 KB
    
    📄 CommandBuilders.lean 7.6 KB
    
    📄 Cpi.lean 9.7 KB
    
    📄 Guards.lean 18.8 KB
    
    📄 SBPF.lean 266 B
    
    📄 Spec.lean 27.7 KB
    
    📄 State.lean 1.9 KB
    
    📄 Valid.lean 1.7 KB
    
    📄 Verify.lean 2.2 KB
  - 📄 Solana.lean 281 B
- 📄 lake-manifest.json 3.1 KB
- 📄 lakefile.lean 505 B
- 📄 lean-toolchain 28 B
- 📄 QEDGen.lean 216 B
- 📄 README.md 6.7 KB
- 📄 test_bridge.lean 2.5 KB
- 📄 test_command_builders.lean 7.2 KB
- 📄 test_guards.lean 4.3 KB
- 📄 test_guards_dropset.lean 13.2 KB
- 📄 test_lemmas.lean 2.3 KB
- 📄 test_property.lean 8.5 KB
- 📄 test_slippage_bridge.lean 3.8 KB
- 📄 test_spec.lean 16.4 KB
- 📄 test_verify.lean 891 B
📁 lean_solana_mathlib/
- 📁 QEDGenMathlib/
  - 📄 IndexedState.lean 5.4 KB
- 📄 lakefile.lean 986 B
- 📄 lean-toolchain 28 B
📁 references/
- 📄 adversarial-probes.md 12.7 KB
- 📄 brownfield-testing.md 1.6 KB
- 📄 cli.md 27.8 KB
- 📄 kani-examples.md 1.8 KB
- 📄 proof-patterns.md 4.6 KB
- 📄 qedspec-anchor.md 10.7 KB
- 📄 qedspec-dsl.md 38.4 KB
- 📄 qedspec-imports.md 9.9 KB
- 📄 release-history.md 2.4 KB
- 📄 sbpf.md 13.4 KB
- 📄 skill-operations.md 1.4 KB
- 📄 support-library.md 5.6 KB
📁 scripts/
- 📄 check-lake-build.sh 3.2 KB
- 📄 check-readme-drift.sh 2.0 KB
- 📄 check-version-consistency.sh 1.0 KB
📁 skills/
- 📁 qedgen-auditor/
  - 📄 exploits.md 63.2 KB
  - 📄 SKILL.md 60.1 KB
📁 templates/
- 📁 prompts/
  - 📄 sbpf_sorry_fill_prompt.txt 1.1 KB
  - 📄 sbpf_system_prompt.txt 1.4 KB
  - 📄 sorry_fill_prompt.txt 771 B
  - 📄 system_prompt.txt 1.2 KB
- 📄 verify.yml 944 B
📁 tools/
- 📄 qedgen 357 B
📄 .gitattributes 578 B
📄 .gitignore 1.5 KB
📄 .npmignore 352 B
📄 Cargo.lock 50.2 KB
📄 Cargo.toml 669 B
📄 claude.md 23.7 KB
📄 install.sh 5.6 KB
📄 LICENSE 1.0 KB
📄 Makefile 187 B
📄 package.json 1022 B
📄 README.md 20.8 KB
📄 SKILL.md 8.0 KB

SKILL.md

---
name: qedgen
description: Find the bugs your tests miss. Define what your Solana program must guarantee in a .qedspec; QEDGen validates it, generates tests and proofs, and scaffolds agent-fill Rust code. Trigger when the user asks for "qedgen", "qedspec", "verify my code", "prove correctness", formal verification, property testing, generated Kani/proptest/Lean artifacts, or Solana program correctness.
---

# QEDGen

## Trigger And Mission

Use this skill when the user wants to verify Solana program behavior, write or review a `.qedspec`, generate verification artifacts, onboard an existing Anchor program, or keep generated artifacts in sync.

Mission:
- Read the source before writing the spec.
- Treat `.qedspec` as the single source of truth.
- Use `qedgen check` to validate the spec.
- Use `qedgen codegen` to scaffold generated artifacts.
- Fill generated Rust handler TODOs as an agent task, then build and test.
- Use `qedgen verify` and drift gates to keep proofs and code synchronized.

Do not present generated Rust as complete business logic. Anchor and Quasar output is an implementation scaffold. Handler files can intentionally contain `todo!()` for transfers, events, CPI wiring, and non-mechanical effects until the agent fills them.

## How To Run QEDGen

Prefer the installed skill wrapper when available:

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

From a repo checkout, the local binary also works:

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

Every write path expects a git repo. If the command errors outside a repo, run `git init` or move into the project root.

Common commands:

```bash
$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/
```

Release and repo-maintenance gates:

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

Read `references/cli.md` for the full CLI surface and flags.

## Flow: Validate -> Scaffold -> Fill -> Verify

Step 1. Understand the program.

Read the Rust source, tests, account model, authorities, PDAs, token flows, arithmetic, and lifecycle. For a returning QEDGen project, read the `.qedspec` next to the code. Do not treat `Spec.lean` as source; it is generated.

Step 2. Validate the spec.

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

Fix lint, coverage, import, lifecycle, arithmetic, and CPI-shape findings in the `.qedspec` first. The spec should describe the intended behavior before codegen or proof work begins.

Step 3. Scaffold generated artifacts.

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

Use `--target quasar` for Quasar. Pinocchio is reserved and should not be promised as complete.

Step 4. Fill generated Rust.

Open generated handler files that contain `todo!()`. Fill business logic using the guard calls, state structs, and spec effects as the contract. Then run the framework build and tests until compile-clean:

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

Step 5. Verify generated backends.

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

Run only the backends relevant to artifacts present in the project. For generated examples in this repo, also run:

```bash
$QEDGEN check --regen-drift
```

## Brownfield Onboarding

For an existing Anchor program:

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

Then fill TODOs in the `.qedspec`, validate it, and cross-check against the live program:

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

After the spec covers each handler, stamp source drift attributes:

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

Paste the emitted `#[qed(verified, ...)]` attributes above the matching handler functions. Future handler-body, accounts-constraint, or spec edits should fail the build until the attributes are intentionally refreshed.

If handler dispatch is non-standard, use explicit overrides:

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

For IDL-only onboarding:

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

IDL scaffolds are shape-only. They need source review before they can express semantic guarantees.

## Codegen Ownership

Generated and always safe to regenerate:

| Path | Owner | Notes |
|---|---|---|
| `Cargo.toml` | QEDGen | Framework dependencies and macro dependency |
| `src/state.rs` | QEDGen | Account/state structs and lifecycle status |
| `src/events.rs` | QEDGen | Event structs |
| `src/errors.rs` | QEDGen | Error enum plus operational variants |
| `src/guards.rs` | QEDGen | Requires, aborts, lifecycle, PDA, and token-authority checks |
| `src/math.rs` | QEDGen | Emitted only when helper arithmetic is needed |
| `src/instructions/mod.rs` | QEDGen | Module declarations and Quasar re-exports |
| `tests/kani.rs` | QEDGen | Kani harnesses |
| `tests/proptest.rs` | QEDGen | Property-test harnesses |
| `src/tests.rs` | QEDGen | Unit tests when requested |
| `src/integration_tests.rs` | QEDGen | Integration-test scaffold when requested |
| `formal_verification/Spec.lean` | QEDGen | Lean model generated from `.qedspec` |

User-owned after first scaffold:

| Path | Owner | Notes |
|---|---|---|
| `src/lib.rs` | User or agent | Crate shell can gain custom imports/modules |
| `src/instructions/<handler>.rs` | User or agent | Business logic and generated TODOs live here |
| `formal_verification/Proofs.lean` | User or agent | Durable Lean proofs |
| Existing project tests | User or agent | Do not replace with generated tests |

Generated support code should compile around intentional handler TODOs. If support code fails to compile, fix the generator or generated support. If handler business logic is missing, fill the handler.

## Proof Handoff

Use proof engineering only when tests and bounded model checking are insufficient.

Use proptest for:
- Fast counterexamples during spec iteration.
- Randomized state transitions.
- Cheap regression checks.

Use Kani for:
- Access control.
- Arithmetic safety.
- Conservation and isolation invariants.
- Bounded state-machine properties.

Use Lean for:
- DeFi math that needs symbolic reasoning beyond bounded search.
- Wide arithmetic solvency arguments.
- Inductive sBPF bytecode proofs.
- Proof obligations where Kani/proptest cannot give enough confidence.

Use Leanstral for routine sorry filling and Aristotle for harder long-running proof search. Read `references/proof-patterns.md` before proof repair and `references/sbpf.md` for sBPF.

Always run `lake build` after editing Lean and run `qedgen check` after proofs compile so orphan or missing obligations are reported.

## References

Load references on demand. Do not bulk-load all files.

| Reference | Use When |
|---|---|
| `references/cli.md` | Full command and flag details |
| `references/qedspec-dsl.md` | DSL syntax and modeling patterns |
| `references/qedspec-imports.md` | `import`, `qed.toml`, `qed.lock`, `--frozen`, upstream checks |
| `references/qedspec-anchor.md` | Anchor adapter and brownfield coverage checks |
| `references/adversarial-probes.md` | Agent-walked attack-surface checklist |
| `references/proof-patterns.md` | Lean proof tactics and repair patterns |
| `references/support-library.md` | Lean support library types and lemmas |
| `references/sbpf.md` | sBPF assembly verification |
| `references/kani-examples.md` | Longer Kani harness examples moved out of the skill |
| `references/brownfield-testing.md` | Existing-test strategy for brownfield projects |
| `references/skill-operations.md` | Git hygiene, learning capture, environment, and error handling |
| `references/release-history.md` | Version-feature history moved out of the skill |

登录后下载/点赞/收藏 ❤ 52 | ★ 0

qedgen

目录结构

SKILL.md

举报内容

提示