Dafny中位向量验证因堆变量使用差异引发超时问题问询

一、验证超时问题分析 #

重现代码 #

class Repro {
  var a: bv32

  function myEnc(v: (bv32, bv32), sum: bv32, DUMMY_PLACEHOLDER: bv32): bv32 
  reads this`a
  {
    (((v.1 << 4) + a))
  }

  lemma myEncLemma_fast(v: (bv32, bv32), sum: bv32) {
    assert 
      myEnc(v, sum, a) ==
      (((v.1 << 4) + a));
  }

  lemma myEncLemma_slow(v: (bv32, bv32), sum: bv32) {
    assert 
      myEnc(v, sum, 0) ==
      (((v.1 << 4) + a));
  }
}

验证命令与输出 #

执行命令：

~/Downloads/dafny/dafny verify --progress Symbol mini_repro.dfy

验证结果：

❯ ~/Downloads/dafny/dafny verify --progress Symbol mini_repro.dfy
Verified 0/3 symbols. Waiting for Repro.myEnc to verify.
Verified 1/3 symbols. Waiting for Repro.myEncLemma_fast to verify.
Verified 2/3 symbols. Waiting for Repro.myEncLemma_slow to verify.
mini_repro.dfy(16,8): Error: Verification of 'Repro.myEncLemma_slow' timed out after 30 seconds. (the limit can be increased using --verification-time-limit)
   |
16 |   lemma myEncLemma_slow(v: (bv32, bv32), sum: bv32) {
   |         ^^^^^^^^^^^^^^^


Dafny program verifier finished with 2 verified, 0 errors, 1 time out

问题原因分析 #

• 两个引理的核心差异仅在于调用myEnc时传入的第三个参数：myEncLemma_fast传入堆字段a，myEncLemma_slow传入常量0。
• 移除左移位操作后，myEncLemma_slow可快速验证；直接将myEnc的定义内联到引理中，两个引理都能快速通过。

这确实和Dafny对堆变量的编码方式有关：
Dafny处理堆变量时会引入额外的约束（比如reads子句对应的堆一致性逻辑）。当传入常量0而非堆变量时，SMT求解器需要处理的等式展开和约束组合更复杂，再加上位运算（左移）的存在，进一步提升了求解难度，最终导致超时。而传入堆变量a时，验证器可以利用reads子句的信息，直接关联函数体内的a与传入的参数a，减少了求解器需要处理的分支，因此能快速完成验证。

二、新版Dafny生成Boogie/SMT文件的方法 #

针对Dafny 4.11.0版本，可通过以下命令生成对应文件：

生成Boogie文件 #

使用compile命令搭配--boogie参数：

dafny compile --boogie mini_repro.dfy

执行后会生成同名的.bpl格式Boogie文件。

生成SMT文件 #

需分两步操作：

1. 先按上述方法生成Boogie文件
2. 使用Boogie工具的/smtProverLog参数输出SMT交互日志：

boogie /smtProverLog:mini_repro.smt mini_repro.bpl

也可通过Dafny的verify命令加--trace参数查看SMT交互过程，若需要完整的SMT文件，上述两步法更直接。

内容的提问来源于stack exchange，提问作者bobismijnnaam