本机 int 的以 2 为底的指数

Question

一些算法（分配二叉树...）需要计算以 2 为底的指数。如何为本机类型计算它？

newtype {:nativeType "uint"} u32 =
  x: nat | 0 <= x < 2147483648

这是一个明显的尝试：

function pow2(n: u32): (r: u32)
  requires n < 10
{
  if n == 0 then 1 else 2 * pow2(n - 1)
}

它失败了，因为 Dafny 怀疑产品保持在 u32 的最大值以下。如何证明它的值在2**10以下？

Answer 1

在这种情况下，更方便的是先定义函数的无界版本，然后证明一个引理表明当n < 10（或n < 32，甚至）是在界内.

function pow2(n: nat): int
{
  if n == 0 then 1 else 2 * pow2(n - 1)
}

lemma pow2Bounds(n: nat)
    requires n < 32
    ensures 0 <= pow2(n) < 0x100000000
{ /* omitted here; two proofs given below */ }

function pow2u32(n: u32): u32
    requires n < 32
{
    pow2Bounds(n as nat);
    pow2(n as nat) as u32
}

直觉上，我们可能希望引理自动通过，因为只有少数情况需要考虑：n = 0、n = 1、... n = 31。但 Dafny 不会自动执行此类案例分析。相反，我们有几个选择。

第一个证明

首先，我们可以证明一个更一般的属性，由于归纳推理的魔力，更容易证明，尽管它比我们需要的更强大.

lemma pow2Monotone(a: nat, b: nat)
    requires a < b
    ensures pow2(a) < pow2(b)
{}  // Dafny is able to prove this automatically by induction.

接下来是引理。

lemma pow2Bounds(n: nat)
    requires n < 32
    ensures 0 <= pow2(n) < 0x100000000
{
    pow2Monotone(n, 32);
}

第二次证明

证明它的另一种方法是告诉 Dafny 它应该展开 pow2 最多 32 次，使用 :fuel 属性。这32个展开本质上就是让Dafny对每个可能的值做个案分析。然后 Dafny 可以在没有额外帮助的情况下完成证明。

lemma {:fuel pow2,31,32} pow2Bounds(n: nat)
    requires n < 32
    ensures 0 <= pow2(n) < 0x100000000
{}

:fuel 属性在第 24 节的 Dafny Reference Manual 中有（轻微）记录。

Answer 2

有点作弊，但对于如此狭窄的域，这非常有效。

const pow2: seq<u32> :=
  [0x1, 0x2, 0x4, 0x8, 0x10, 0x20];

lemma pow2_exponential(n: u32)
  ensures n == 0    ==> pow2[n] == 1
  ensures 0 < n < 6 ==> pow2[n] == 2 * pow2[n - 1]  
{}

本机 int 的以 2 为底的指数

Base 2 exponential of native int

native

dafny

第一个证明

第二次证明