咨询：Dafny为何无法识别bv64右移操作会减小数值

你编写的Dafny引理使用bv64类型参数，递归时传入input >> 7，却被提示decreases clause might not decrease，核心原因在于以下两点：

核心原因 #

1. 位向量的语义特性：bv64是无符号位向量，右移>>是逻辑右移，但Dafny不会自动将位向量的大小关系和整数的全序关系划等号。尤其当input为0时，input >>7仍然是0，此时递归参数完全没有递减，这是Dafny能检测到的反例。
2. 自动推理的局限性：即便input非0，Dafny的自动定理证明器不会主动展开位向量右移的语义细节来证明input >>7 < input，需要明确的引导或辅助引理来建立这个关系。

可行的解决办法 #

1. 排除0的输入前提 #

如果你的引理不需要处理输入为0的情况，直接添加前提并补充断言：

lemma Shift(input: bv64)
    requires input != 0
    decreases input
{
    assert input >> 7 < input;
    Shift(input >> 7);
}

若Dafny仍不认可该断言，可补充辅助引理强化证明：

lemma BvRightShiftLess(input: bv64)
    requires input != 0
    ensures input >> 7 < input
{
    let int_val := input as int;
    assert int_val > 0;
    assert (input >> 7 as int) == int_val / 128;
    assert int_val / 128 < int_val;
}

lemma Shift(input: bv64)
    requires input != 0
    decreases input
{
    BvRightShiftLess(input);
    Shift(input >> 7);
}

2. 改用整数作为递减度量 #

将位向量转换为整数，利用整数的递减关系让Dafny更容易验证：

lemma Shift(input: bv64)
    requires input != 0
    decreases input as int
{
    Shift(input >> 7);
}

3. 处理0的情况避免无限递归 #

如果需要支持输入为0，添加分支终止递归：

lemma Shift(input: bv64)
    decreases input
{
    if input != 0 {
        assert input >> 7 < input;
        Shift(input >> 7);
    }
}

总结 #

• 位向量与整数的语义差异是核心障碍，Dafny不会默认关联二者的大小关系；
• 输入为0是递减不成立的直接反例，必须明确处理；
• 通过添加前提、辅助引理或转换度量类型，可帮助Dafny完成递减性证明。

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