我有以下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
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

如你所见，"fast" 引理可以立即通过验证，而 "slow" 引理则超时。唯一的区别是，在快速引理中通过字段a 提及了堆，而在慢速引理中没有。如果我在所有地方去掉左移运算，慢速引理也会变得像快速引理一样。这究竟怎么回事？在两个引理中用 myEnc 的定义替换，也能让验证更快。不知为何，堆变量的编码似乎干扰了等式证明？

我不确定如何让Dafny生成Boogie/SMT文件。新的CLI似乎并未暴露这个选项。

我正在使用Dafny 4.11.0+fcb2042d6d043a2634f0854338c08feeaaaf4ae2，目前从GitHub发布的最新版本。

解决方案

你需要在引理上指定一个后置条件，否则它们不会真的有用。指定后置条件并验证通过后，你就可以调用它们来应用前置条件和后置条件，从而向验证器证明更强大但并非完全直观的事实。

你可以在这里找到更多示例：https://dev.to/hath995/dafny-programming-language-and-software-verification-system-2afi

module SOBV {
    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 extraneous(v: (bv32, bv32), sum: bv32)
    ensures forall ph: bv32 :: true ==> myEnc(v, sum, ph) == myEnc(v, sum, 0)
  {
  }

  lemma bh(v: (bv32, bv32), sum: bv32, placeholder: bv32)
    ensures myEnc(v, sum, placeholder) == myEnc(v, sum, 0)
  {
  }

  lemma myEncLemma_slow(v: (bv32, bv32), sum: bv32) {
    //extraneous(v, sum); //works but is slow
    // bh(v, sum, 0); //same as above
    // bh(v, sum, a); //works quite fast
    assert 
      myEnc(v, sum, 0) ==
      (((v.1 << 4) + a));
  }
    }
}

编辑：另一种方案

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