qedgen

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

通过编写 Lean 4 证明来正式验证程序。每当用户想要正式验证代码、生成 Lean 4 证明、证明算法或智能合约的属性、验证不变量、将程序逻辑转换为正式规范或涉及 Lean 4 和形式验证的任何内容时，即可触发此技能。当用户提到“qedgen”、“精益证明”、“形式证明”、“验证我的代码”、“证明正确性”、“形式验证”或想要对其实现进行数学保证时也会触发。

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

目录结构

当前层级: tree/main/

📁 .github/
- 📁 workflows/
  - 📄 release.yml 1.6 KB
📁 crates/
- 📁 qedgen/
  - 📁 src/
    
    📄 api.rs 38.9 KB
    
    📄 asm2lean.rs 26.2 KB
    
    📄 consolidate.rs 6.2 KB
    
    📄 main.rs 4.7 KB
    
    📄 project.rs 3.0 KB
    
    📄 spec.rs 19.4 KB
    
    📄 validate.rs 5.6 KB
  - 📁 templates/
    
    📄 .gitignore 29 B
    
    📄 lakefile.lean 292 B
    
    📄 lean-toolchain 25 B
    
    📄 Main.lean 154 B
    
    📄 PROMPT_TEMPLATE.md 3.2 KB
    
    📄 README.lean.md 1.6 KB
  - 📄 Cargo.toml 544 B
📁 docs/
- 📄 CNAME 10 B
- 📄 index.html 11.6 KB
- 📄 llms-full.txt 8.7 KB
- 📄 llms.txt 2.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.png 38.2 KB
- 📄 qgn_demo.html 69.3 KB
- 📄 style.css 8.1 KB
📁 examples/
- 📁 rust/
  - 📁 escrow/
    
    📁 formal_verification/
    
    📄 .gitignore 87 B
    
    📄 EscrowProofs.lean 9.3 KB
    
    📄 lake-manifest.json 3.2 KB
    
    📄 lakefile.lean 273 B
    
    📄 lean-toolchain 25 B
    
    📄 README.md 674 B
    
    📄 SPEC.md 6.5 KB
    
    📄 VERIFICATION_SCOPE.md 5.4 KB
    
    📁 migrations/
    
    📄 deploy.ts 428 B
    
    📁 programs/
    
    📁 escrow/
    
    📁 src/
    
    📄 lib.rs 6.7 KB
    
    📄 Cargo.toml 376 B
    
    📄 Xargo.toml 62 B
    
    📁 tests/
    
    📄 escrow.ts 8.6 KB
    
    📄 .gitignore 67 B
    
    📄 .prettierignore 61 B
    
    📄 Anchor.toml 353 B
    
    📄 Cargo.lock 72.8 KB
    
    📄 Cargo.toml 215 B
    
    📄 package.json 528 B
    
    📄 tsconfig.json 205 B
  - 📁 percolator/
    
    📁 .cargo/
    
    📄 config.toml 33 B
    
    📁 examples/
    
    📄 offsets.rs 1.3 KB
    
    📁 formal_verification/
    
    📄 lake-manifest.json 3.2 KB
    
    📄 lakefile.lean 291 B
    
    📄 lean-toolchain 25 B
    
    📄 PercolatorProofs.lean 7.6 KB
    
    📄 SPEC.md 4.6 KB
    
    📁 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
    
    📄 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
    
    📄 unit_tests.rs 93.8 KB
    
    📄 .gitignore 320 B
    
    📄 Cargo.lock 8.5 KB
    
    📄 Cargo.toml 639 B
    
    📄 LICENSE 11.1 KB
    
    📄 README.md 4.9 KB
    
    📄 spec.md 108.4 KB
- 📁 sbpf/
  - 📁 counter/
    
    📁 formal_verification/
    
    📄 CounterProg.lean 22.1 KB
    
    📄 CounterProofs.lean 6.3 KB
    
    📄 lake-manifest.json 317 B
    
    📄 lakefile.lean 237 B
    
    📄 lean-toolchain 25 B
    
    📁 src/
    
    📄 counter.s 22.9 KB
  - 📁 slippage/
    
    📁 formal_verification/
    
    📄 lake-manifest.json 318 B
    
    📄 lakefile.lean 242 B
    
    📄 lean-toolchain 25 B
    
    📄 SlippageProg.lean 912 B
    
    📄 SlippageProofs.lean 1.5 KB
    
    📄 SPEC.md 2.5 KB
    
    📁 src/
    
    📁 asm-slippage/
    
    📄 asm-slippage.s 698 B
  - 📁 transfer/
    
    📁 formal_verification/
    
    📄 lake-manifest.json 318 B
    
    📄 lakefile.lean 242 B
    
    📄 lean-toolchain 25 B
    
    📄 SPEC.md 3.6 KB
    
    📄 TransferProg.lean 3.2 KB
    
    📄 TransferProofs.lean 3.3 KB
    
    📁 src/
    
    📄 transfer.s 2.4 KB
  - 📁 tree/
    
    📁 formal_verification/
    
    📄 lake-manifest.json 314 B
    
    📄 lakefile.lean 222 B
    
    📄 lean-toolchain 25 B
    
    📄 TreeProg.lean 59.2 KB
    
    📄 TreeProofs.lean 8.3 KB
    
    📁 src/
    
    📄 tree.s 61.1 KB
📁 lean_solana/
- 📁 QEDGen/
  - 📁 Solana/
    
    📁 SBPF/
    
    📄 Execute.lean 12.2 KB
    
    📄 ISA.lean 5.1 KB
    
    📄 Memory.lean 6.1 KB
    
    📄 Tactic.lean 2.3 KB
    
    📄 Account.lean 4.0 KB
    
    📄 Authority.lean 285 B
    
    📄 Cpi.lean 9.0 KB
    
    📄 SBPF.lean 130 B
    
    📄 State.lean 1.9 KB
    
    📄 Valid.lean 2.0 KB
  - 📄 Solana.lean 165 B
- 📄 lake-manifest.json 119 B
- 📄 lakefile.lean 112 B
- 📄 lean-toolchain 25 B
- 📄 QEDGen.lean 165 B
- 📄 README.md 2.5 KB
- 📄 test_lemmas.lean 2.3 KB
📁 tools/
- 📄 qedgen 357 B
📄 .gitignore 777 B
📄 .npmignore 352 B
📄 Cargo.lock 38.2 KB
📄 Cargo.toml 347 B
📄 claude.md 9.7 KB
📄 install.sh 5.5 KB
📄 LICENSE 1.0 KB
📄 package.json 762 B
📄 README.md 4.1 KB
📄 SKILL.md 21.0 KB

SKILL.md

---
name: qedgen
description: Formally verify programs by writing Lean 4 proofs. Trigger this skill whenever the user wants to formally verify code, generate Lean 4 proofs, prove properties about algorithms or smart contracts, verify invariants, convert program logic into formal specifications, or anything involving Lean 4 and formal verification. Also trigger when the user mentions "qedgen", "lean proof", "formal proof", "verify my code", "prove correctness", "formal verification", or wants mathematical guarantees about their implementation.
---

# QEDGen — Agent-Driven Formal Verification

You (Claude) are the proof engineer. You read the codebase, write Lean 4 models and proofs, iterate on compiler errors, and call Leanstral (Mistral's theorem prover) only for hard sub-goals you cannot fill yourself.

## Important: how to run qedgen

All `qedgen` commands in this document MUST be run via the wrapper script at `tools/qedgen` inside the skill directory (`~/.agents/skills/qedgen/tools/qedgen`). The wrapper auto-installs the binary on first use — downloading the correct platform binary from GitHub releases, or compiling from source as a fallback.

Set this once at the start and use it for every command:
```bash
QEDGEN="$HOME/.agents/skills/qedgen/tools/qedgen"
```

## Architecture

```
You (Claude)                          Leanstral (remote model)
  ├── Read spec / source code           ├── Fill sorry markers
  ├── Write Lean 4 models               └── Suggest tactics for hard goals
  ├── Write theorem statements
  ├── Write proof attempts
  ├── Run `lake build`, read errors
  └── Fix and iterate
```

## Step 1: Understand the program

Check for existing artifacts in this priority order:

1. **spec.md exists** → Read it. An existing spec captures the author's intent, state model, invariants, and operations. Extract security goals, state model, and formal properties. Skip the scoping quiz and go directly to Step 2.
2. **IDL exists** (`target/idl/<program>.json`) → Run `$QEDGEN spec --idl <path>` to generate a draft SPEC.md with TODO markers, then refine interactively.
3. **Neither exists** → Read the source code directly. Ask broader scoping questions.

## Step 2: Scope the verification

If no spec.md was found, run a short interactive quiz — one question at a time, with checkbox options derived from the program's structure. Ask about **functionality and risks**, not implementation details.

**Question 1: "What does this program need to guarantee above all else?"**
Options derived from the program's structure:
- Authorization / access control
- Tokens are never lost / correct routing
- One-shot safety / no replay
- Arithmetic safety / no overflow
- Conservation (e.g., vault >= total claims)
- All of the above

**Question 2: "Which scenario worries you most?"**
Generate concrete risk scenarios from the program.

**Question 3: "Does the program make any assumptions that aren't enforced on-chain?"**

Ask questions **one at a time**. Wait for the user's answer before presenting the next question.

## Step 3: Write SPEC.md

Write `formal_verification/SPEC.md` using normative language (MUST, MUST NOT, MAY). Structure:

```markdown
# <Program Name> Verification Spec v1.0

<1-2 sentences describing what the program does>

## 0. Security Goals
1. **<Goal name>**: <normative statement>

## 1. State Model
<State struct with field names, types, and comments>
<Lifecycle diagram if applicable>

## 2. Operations
### 2.1 <Operation name>
**Signers**: <who MUST sign>
**Preconditions**: <what MUST be true before>
**Effects**: <numbered steps>
**Postconditions**: <what MUST be true after>

## 3. Formal Properties
### 3.1 <Category>
**<property_id>**: For all <quantified variables>,
if <transition predicate> then <conclusion>.

## 4. Trust Boundary
<What is axiomatic and why>

## 5. Verification Results
| Property | Status | Proof |
|---|---|---|
| ... | **Open** | |
```

Present SPEC.md to the user and get confirmation before proceeding.

## Step 4: Set up the Lean project

```bash
$QEDGEN setup            # Ensure global Mathlib cache exists (first time: 15-45 min)
```

Create the project structure:

```
formal_verification/
  lakefile.lean          # require qedgenSupport from path/to/lean_solana
  lean-toolchain         # leanprover/lean4:v4.15.0
  Proofs.lean            # root import: import Proofs.AccessControl etc.
  Proofs/
    AccessControl.lean
    CpiCorrectness.lean
    Conservation.lean
    StateMachine.lean
    ArithmeticSafety.lean
```

## Step 5: Write Lean proofs

This is the core step. You write Lean 4 directly — models, transitions, theorems, and proofs.

### Modeling workflow

For each property in SPEC.md:

1. **Define the state** as a Lean structure (map fields from source/spec)
2. **Define the transition** as `Option StateType` (return `none` on precondition failure)
3. **State the theorem** matching the SPEC.md property
4. **Write the proof** using the patterns below
5. **Run `lake build`** and iterate on errors

### Support library API

After `import QEDGen.Solana` and `open QEDGen.Solana`:

**Types:**
- `Pubkey` (= Nat), `U64` (= Nat), `U8` (= Nat)
- `Account` — `{ key : Pubkey, authority : Pubkey, balance : Nat, writable : Bool }`
- `Lifecycle` — `open | closed` (with DecidableEq)
- `AccountMeta` — `{ pubkey : Pubkey, isSigner : Bool, isWritable : Bool }`
- `CpiInstruction` — `{ programId : Pubkey, accounts : List AccountMeta, data : List Nat }`

**Constants:**
- `SYSTEM_PROGRAM_ID`, `TOKEN_PROGRAM_ID`, `TOKEN_2022_PROGRAM_ID`, `ASSOCIATED_TOKEN_PROGRAM_ID`
- `MEMO_PROGRAM_ID`, `COMPUTE_BUDGET_PROGRAM_ID`, `STAKE_PROGRAM_ID`
- `DISC_TRANSFER`, `DISC_TRANSFER_CHECKED`, `DISC_MINT_TO`, `DISC_BURN`, `DISC_CLOSE_ACCOUNT`, etc.
- `DISC_SYS_CREATE_ACCOUNT`, `DISC_SYS_TRANSFER`, etc.
- `DISC_ATA_CREATE`, `DISC_ATA_CREATE_IDEMPOTENT`
- `U8_MAX`, `U16_MAX`, `U32_MAX`, `U64_MAX`, `U128_MAX`

**Functions:**
- `findByKey : List Account → Pubkey → Option Account`
- `findByAuthority : List Account → Pubkey → Option Account`
- `canWrite : Pubkey → Account → Prop`
- `targetsProgram : CpiInstruction → Pubkey → Prop`
- `accountAt : CpiInstruction → Nat → Pubkey → Bool → Bool → Prop`
- `hasDiscriminator : CpiInstruction → List Nat → Prop`
- `hasNAccounts : CpiInstruction → Nat → Prop`
- `cpiWellFormed : CpiInstruction → Prop`
- `closes : Lifecycle → Lifecycle → Prop`
- `valid_u64 : Nat → Prop` (and u8, u16, u32, u128)

**Key lemmas:**
- `closes_is_closed`, `closes_was_open`, `closed_irreversible`
- `valid_u64_preserved_by_zero`, `valid_u64_preserved_by_same`
- `find_map_update_other`, `find_map_update_same` (axioms for account list updates)

### Proof patterns

**Access control** — signer must match authority:
```lean
structure ProgramState where
  authority : Pubkey

def cancelTransition (s : ProgramState) (signer : Pubkey) : Option Unit :=
  if signer = s.authority then some () else none

theorem cancel_access_control (s : ProgramState) (signer : Pubkey)
    (h : cancelTransition s signer ≠ none) :
    signer = s.authority := by
  unfold cancelTransition at h
  split_ifs at h with h_eq
  · exact h_eq
  · contradiction
```

**CPI correctness** — program, accounts, discriminator match (pure `rfl`):
```lean
def cancel_build_cpi (ctx : CancelContext) : CpiInstruction :=
  { programId := TOKEN_PROGRAM_ID
  , accounts := [
      ⟨ctx.escrow_token, false, true⟩,   -- source: writable
      ⟨ctx.dest, false, true⟩,            -- dest: writable
      ⟨ctx.authority, true, false⟩         -- authority: signer
    ]
  , data := [DISC_TRANSFER]
  }

theorem cancel_cpi_correct (ctx : CancelContext) :
    let cpi := cancel_build_cpi ctx
    targetsProgram cpi TOKEN_PROGRAM_ID ∧
    accountAt cpi 0 ctx.escrow_token false true ∧
    accountAt cpi 1 ctx.dest false true ∧
    accountAt cpi 2 ctx.authority true false ∧
    hasDiscriminator cpi [DISC_TRANSFER] := by
  unfold cancel_build_cpi targetsProgram accountAt hasDiscriminator
  exact ⟨rfl, rfl, rfl, rfl, rfl⟩
```

**State machine** — lifecycle transitions:
```lean
def cancelTransition (s : ProgramState) : Option ProgramState :=
  if s.escrow.lifecycle = Lifecycle.open then
    some { escrow := { s.escrow with lifecycle := Lifecycle.closed } }
  else none

theorem cancel_closes_escrow (pre post : ProgramState)
    (h : cancelTransition pre = some post) :
    post.escrow.lifecycle = Lifecycle.closed := by
  unfold cancelTransition at h
  split_ifs at h with h_open
  cases h
  rfl
```

**Conservation** — invariant preserved across operations:
```lean
def conservation (s : EngineState) : Prop := s.V >= s.C_tot + s.I

def depositTransition (s : EngineState) (amount : Nat) : Option EngineState :=
  if s.V + amount <= MAX_VAULT_TVL then
    some { V := s.V + amount, C_tot := s.C_tot + amount, I := s.I }
  else none

theorem deposit_conservation (s s' : EngineState) (amount : Nat)
    (h_inv : conservation s)
    (h : depositTransition s amount = some s') :
    conservation s' := by
  unfold depositTransition at h
  split_ifs at h with h_le
  · cases h
    unfold conservation at h_inv ⊢  -- MUST unfold in BOTH hypothesis and goal
    omega
  · contradiction
```

**Arithmetic safety** — bounds preserved:
```lean
def initializeTransition (amount taker : Nat) : Option ProgramState :=
  if amount > 0 ∧ amount ≤ U64_MAX ∧ taker > 0 ∧ taker ≤ U64_MAX then
    some { initializer_amount := amount, taker_amount := taker }
  else none

theorem initialize_arithmetic_safety (amount taker : Nat) (post : ProgramState)
    (h : initializeTransition amount taker = some post) :
    post.initializer_amount ≤ U64_MAX ∧ post.taker_amount ≤ U64_MAX := by
  unfold initializeTransition at h
  split_ifs at h with h_bounds
  cases h
  exact ⟨h_bounds.2.1, h_bounds.2.2.2⟩
```

### Critical tactic rules

| Do | Don't |
|---|---|
| `unfold f at h` before `split_ifs` | `simp [f] at h` before `split_ifs` (kills if-structure) |
| `unfold pred at h_inv ⊢` for named predicates | `unfold pred` only in goal (omega can't see hypotheses) |
| `cases h` after `split_ifs` on `some = some` | `injection h` (unnecessary, cases handles it) |
| `omega` for linear arithmetic | `norm_num` for linear goals (omega is more reliable) |
| `exact ⟨rfl, rfl, rfl⟩` for conjunctions of rfl | `constructor` + `rfl` + `constructor` + `rfl` (verbose) |
| `if cond then ... else ...` without proof binding | `if h : cond then ...` when `h` is unused |

### Common errors and fixes

| Error | Fix |
|---|---|
| `omega could not prove the goal` | Unfold named predicates in hypotheses: `unfold pred at h ⊢` |
| `no goals to be solved` | Remove redundant tactic (e.g., `· contradiction` after auto-closed branch) |
| `unknown constant 'X'` | Check imports; add `import QEDGen.Solana.X` or `open QEDGen.Solana` |
| `tactic 'split_ifs' failed, no if-then-else` | Use `unfold` first, not `simp` |
| `unused variable 'h'` | Remove proof binding: `if h : cond` → `if cond` |

## sBPF Assembly Verification

The same workflow applies to hand-written sBPF assembly programs. Claude reads the `.s` source (and IDL if available), writes SPEC.md, then writes Lean proofs using the SBPF support library.

### Reading assembly source

sBPF assembly uses AT&T-like syntax. Reference for understanding the source (transpilation is automated by `asm2lean`):

| Assembly | Lean encoding | Meaning |
|---|---|---|
| `ldxdw r3, [r1+0x2918]` | `.ldx .dword .r3 .r1 0x2918` | Load 8 bytes from mem[r1+offset] into r3 |
| `ldxb r2, [r1+OFF]` | `.ldx .byte .r2 .r1 OFF` | Load 1 byte from mem[r1+offset] into r2 |
| `lddw r0, 1` | `.lddw .r0 1` | Load 64-bit immediate into r0 |
| `jge r3, r4, label` | `.jge .r3 (.reg .r4) <abs_idx>` | Branch if r3 >= r4 |
| `jne r2, 3, label` | `.jne .r2 (.imm 3) <abs_idx>` | Branch if r2 != 3 |
| `add64 r2, 8` | `.add64 .r2 (.imm 8)` | r2 = r2 + 8 (wrapping) |
| `mov64 r0, 1` | `.mov64 .r0 (.imm 1)` | r0 = 1 |
| `call sol_log_` | `.call .sol_log_` | Invoke syscall |
| `exit` | `.exit` | Exit with code in r0 |

**Jump target resolution**: Assembly uses labels; Lean uses absolute instruction indices (0-based). `asm2lean` resolves these automatically.

**`.equ` constants**: Map to `abbrev` definitions. Constants used in memory operands (`[reg + CONST]`) are typed `Int`; all others are `Nat`.

### Modeling the program

Use `qedgen asm2lean` to transpile the `.s` file into a Lean 4 module automatically:

```bash
$QEDGEN asm2lean --input src/program.s --output formal_verification/ProgramProg.lean
```

This generates a module with:
- `abbrev` definitions for all `.equ` constants (offsets as `Int`, values as `Nat`)
- `@[simp] def prog : Program := #[...]` with named constants and index comments
- A namespace wrapper matching the output filename

Add the generated module to `lakefile.lean`:
```lean
lean_lib ProgramProg where
  roots := #[`ProgramProg]
```

Then import it in the proof file:
```lean
import QEDGen.Solana.SBPF
import ProgramProg

open QEDGen.Solana.SBPF
open QEDGen.Solana.SBPF.Memory
open ProgramProg
```

**Never transcribe assembly by hand** — `asm2lean` handles jump target resolution, constant typing, and syntactic matching automatically.

### SBPF support library API

After `import QEDGen.Solana.SBPF` and `open QEDGen.Solana.SBPF`:

**Types:**
- `Reg` — `.r0` through `.r10` (r10 is read-only frame pointer)
- `Src` — `.reg r` or `.imm v`
- `Width` — `.byte` (1), `.half` (2), `.word` (4), `.dword` (8)
- `Syscall` — `.sol_log_`, `.sol_invoke_signed`, `.sol_get_clock_sysvar`, etc.
- `Insn` — All sBPF instructions (`.lddw`, `.ldx`, `.st`, `.stx`, `.add64`, `.jge`, `.call`, `.exit`, etc.)
- `Program` — `Array Insn`

**State types:**
- `RegFile` — struct with fields `r0..r10 : Nat` (all default 0). `@[simp]` on `get`/`set`.
- `State` — `{ regs : RegFile, mem : Mem, pc : Nat, exitCode : Option Nat }`
- `Mem` — `Nat → Nat` (byte-addressable memory)

**Functions (all `@[simp]`):**
- `RegFile.get (rf : RegFile) : Reg → Nat`
- `RegFile.set (rf : RegFile) (r : Reg) (v : Nat) : RegFile` — r10 writes are silently ignored
- `resolveSrc (rf : RegFile) (src : Src) : Nat`
- `step (insn : Insn) (s : State) : State` — single-instruction semantics
- `execSyscall (sc : Syscall) (s : State) : State` — logging sets r0=0
- `initState (inputAddr : Nat) (mem : Mem) : State` — r1=inputAddr, r10=stack, pc=0
- `wrapAdd`, `wrapSub`, `wrapMul`, `wrapNeg` — 64-bit wrapping arithmetic

**Execution:**
- `execute (prog : Program) (s : State) (fuel : Nat) : State` — use `sbpf_steps` tactic to unroll

**Memory functions (open `QEDGen.Solana.SBPF.Memory`):**
- `effectiveAddr (base : Nat) (off : Int) : Nat`
- `readU8`, `readU16`, `readU32`, `readU64` — little-endian reads
- `writeU8`, `writeU16`, `writeU32`, `writeU64` — little-endian writes
- `readByWidth`, `writeByWidth` — dispatch by `Width`

**Memory constants:**
- `RODATA_START`, `BYTECODE_START`, `STACK_START`, `HEAP_START`, `INPUT_START`

**Tactics:**
- `sbpf_steps` — automatically unrolls `execute`, steps through instructions, resolves branches, and closes the goal. Requires `@[simp]` on `prog`.

**Lemmas:**
- `execute_halted` (`@[simp]`) — halted state is a fixed point
- `execute_step` — unfolds one step: `execute prog s (n+1) = execute prog (step insn s) n`
- `execute_zero` (`@[simp]`) — `execute prog s 0 = s`

**Memory axioms:**
- `readU64_writeU64_same` — read-after-write returns original value
- `readU64_writeU64_disjoint` — non-overlapping write doesn't affect read
- `readU8_writeU64_outside`, `readU64_writeU8_disjoint`

### Proof strategy: `sbpf_steps` tactic

Use the `sbpf_steps` tactic to automatically unroll and simplify sBPF execution. It handles instruction fetch, stepping, branch resolution, and final state extraction in a single call:

```lean
set_option maxHeartbeats 8000000 in
theorem rejects_insufficient_balance
    (inputAddr : Nat) (mem : Mem)
    (minBal tokenBal : Nat)
    (h_min : readU64 mem (effectiveAddr inputAddr MINIMUM_BALANCE) = minBal)
    (h_tok : readU64 mem (effectiveAddr inputAddr TOKEN_ACCOUNT_BALANCE) = tokenBal)
    (h_slip : minBal ≥ tokenBal) :
    (execute prog (initState inputAddr mem) 10).exitCode = some 1 := by
  sbpf_steps
```

**Prerequisites for `sbpf_steps` to work efficiently:**
1. `prog` must have `@[simp]` attribute (handled by `asm2lean`)
2. Offset constants in `prog` must be `Int`, not `Nat` (handled by `asm2lean`)
3. Named constants in `prog` must syntactically match hypothesis names (handled by `asm2lean`)

For theorems with negated conditions, you may need a helper before `sbpf_steps`:
```lean
-- When the hypothesis is ≠ but simp needs ¬(... = ...)
have h_ne3 : ¬(readU64 mem inputAddr = N_ACCOUNTS_EXPECTED) := by rw [h_num]; exact h_ne
sbpf_steps

-- When the hypothesis is ≥ but simp needs ¬(... < ...)
have h_not_lt : ¬(senderLamports < amount) := by omega
sbpf_steps
```

Set `maxHeartbeats` generously: 8M for short paths (3-6 instructions), 16M for full validation paths (15+ instructions).

### Theorem statement pattern

Properties are stated over symbolic memory with hypotheses binding memory reads. Use the named constants from the generated `Prog` module — both in hypotheses and exit codes:

```lean
theorem rejects_insufficient_lamports
    (inputAddr : Nat) (mem : Mem)
    (amount senderLamports : Nat)
    (h_num   : readU64 mem inputAddr = N_ACCOUNTS_EXPECTED)
    (h_sdl   : readU64 mem (effectiveAddr inputAddr SENDER_DATA_LENGTH_OFFSET) = DATA_LENGTH_ZERO)
    (h_rdup  : readU8  mem (effectiveAddr inputAddr RECIPIENT_OFFSET) = NON_DUP_MARKER)
    (h_rdl   : readU64 mem (effectiveAddr inputAddr RECIPIENT_DATA_LENGTH_OFFSET) = DATA_LENGTH_ZERO)
    (h_sdup  : readU8  mem (effectiveAddr inputAddr SYSTEM_PROGRAM_OFFSET) = NON_DUP_MARKER)
    (h_idl   : readU64 mem (effectiveAddr inputAddr INSTRUCTION_DATA_LENGTH_OFFSET) = INSTRUCTION_DATA_LENGTH_EXPECTED)
    (h_amt   : readU64 mem (effectiveAddr inputAddr INSTRUCTION_DATA_OFFSET) = amount)
    (h_bal   : readU64 mem (effectiveAddr inputAddr SENDER_LAMPORTS_OFFSET) = senderLamports)
    (h_insuf : senderLamports < amount) :
    (execute prog (initState inputAddr mem) 20).exitCode = some E_INSUFFICIENT_LAMPORTS := by
  sbpf_steps
```

The `fuel` parameter (20 above) must be large enough for the longest execution path. Count the maximum instructions from entry to exit.

**Critical**: Use `readU8` for byte loads (`ldxb`) and `readU64` for dword loads (`ldxdw`). The read width must match the assembly instruction.

### Critical rules for sBPF proofs

| Do | Don't |
|---|---|
| Use `sbpf_steps` tactic for all sBPF proofs | Manually unroll with `execute_step` (verbose, error-prone) |
| Generate `Prog.lean` with `qedgen asm2lean` | Hand-transcribe assembly into Lean (wrong offsets, missing labels) |
| Use named constants from `Prog.lean` in hypotheses | Use raw numeric literals in hypotheses (simp blowup) |
| Use `Int` for offset constants (memory operands) | Use `Nat` for offsets (forces coercion, simp timeout) |
| Ensure `@[simp]` on `prog` definition | Omit `@[simp]` (sbpf_steps cannot unfold prog) |
| Set `maxHeartbeats` 8M–16M for sBPF proofs | Use default heartbeats (will timeout on 8+ instruction paths) |

### sBPF simp performance (critical)

Three rules that determine whether `sbpf_steps` completes in seconds or times out:

1. **Offset constants MUST be `Int`**: `effectiveAddr` takes `(off : Int)`. If the constant is `Nat`, Lean inserts `↑(NAT_CONST)` coercion at every use, and `simp` cannot efficiently reduce `effectiveAddr base ↑N = effectiveAddr base N`. This alone causes 0.5s → 4+ minute blowup.

2. **Named constants in `prog` MUST match hypothesis names**: `simp` uses syntactic matching. If `prog` has `.ldx .dword .r2 .r1 SENDER_DATA_LENGTH_OFFSET` but the hypothesis uses the raw number `88`, `simp` must unfold every `abbrev` at every subterm at every step — exponential blowup.

3. **`@[simp]` on `prog` is required**: Without it, `sbpf_steps` cannot unfold `prog[pc]?` to fetch instructions.

`qedgen asm2lean` handles all three rules automatically.

## Step 6: Call Leanstral for hard sub-goals

When you have a proof with `sorry` markers you cannot fill after 2-3 attempts:

```bash
$QEDGEN fill-sorry --file formal_verification/Proofs/Hard.lean --validate
```

This sends each `sorry` location to Leanstral with focused context. Review the result — Leanstral may introduce tactics you can learn from for future proofs.

If `fill-sorry` also fails, simplify the theorem statement or split the property into smaller lemmas.

## Step 7: Verify and report

```bash
cd formal_verification && lake build
```

Update SPEC.md verification results table:
- **Verified**: Theorem compiles, no `sorry`
- **Partial**: Proof has `sorry` markers
- **Open**: No compiling proof

## Environment

- **`MISTRAL_API_KEY`** — required for `fill-sorry`. Free from [console.mistral.ai](https://console.mistral.ai)
- **`QEDGEN_VALIDATION_WORKSPACE`** — optional override for global Mathlib cache location

## Error handling

- **First `lake build` is slow**: Mathlib compilation takes 15-45 min on first run. Subsequent builds reuse the cache.
- **`could not resolve 'HEAD' to a commit`**: Remove `.lake/packages/mathlib` and run `lake update`.
- **Rate limiting (429)**: Built-in exponential backoff in `fill-sorry`.

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

qedgen

目录结构

SKILL.md

举报内容

提示