在Dafny中验证幂函数额外性质遇循环问题求助

问题背景 #

已实现以下可通过Dafny验证的幂函数：

function power(x: int, y: int) : int
    requires y >= 0
    ensures y == 0 ==> power(x,y) == 1
    ensures y > 0 && y % 2 == 0 ==> power(x,y) == power(x*x,y/2)
    ensures y > 0 && y % 2 == 1 ==> power(x,y) == x * power(x*x,(y-1)/2)
    decreases y
{
    if y == 0 then
        1
    else if y % 2 == 0 then
        power(x*x, y/2)
    else 
        (x * power(x*x,(y-1)/2))
}

尝试添加以下两个额外的ensures子句时，执行dafny verify test.dfy会陷入无限循环，CPU占用率达100%：

ensures y > 0 ==> power(x, y) == x * power(x, y - 1)
ensures forall a :: 0 <= a <= y ==> power(x, y) == power(x, a) * power(x, y - a)

原因分析 #

原函数采用奇偶分治的递归结构（每次递归将y折半或近折半），但新增的两个性质基于逐次减1的递归逻辑。Dafny的自动验证器无法自动关联两种递归结构的终止关系，导致不断展开函数定义，陷入无限循环。必须通过手动添加归纳引理，分步证明这些性质。

分步验证方案 #

1. 证明幂函数步长性质（第一个额外性质） #

定义归纳引理LemmaPowerStep，通过对y归纳，关联奇偶分治结构与逐次减1的逻辑：

lemma LemmaPowerStep(x: int, y: int)
    requires y > 0
    ensures power(x, y) == x * power(x, y - 1)
    decreases y
{
    if y == 1 {
        // 基础情况：y=1时，直接匹配函数定义
        assert power(x,1) == x * power(x,0);
    } else if y % 2 == 0 {
        let half = y/2;
        LemmaPowerStep(x*x, half); // 对更小的half应用归纳假设
        calc {
            power(x, y);
            == power(x*x, half); // 原函数偶数分支的ensures
            == (x*x) * power(x*x, half - 1); // 归纳假设
            == x * (x * power(x*x, (y-2)/2)); // 代数变形
            == x * power(x, y-1); // 原函数奇数分支定义：y-1是奇数
        }
    } else {
        let k = (y-1)/2;
        // y是奇数且>1，y-1是偶数，直接用原函数分支定义推导
        assert power(x, y-1) == power(x*x, k);
        calc {
            power(x, y);
            == x * power(x*x, k); // 原函数奇数分支定义
            == x * power(x, y-1); // 代入上一行断言
        }
    }
}

2. 证明幂函数分配律（第二个额外性质） #

基于步长性质，通过对y归纳证明分配律，覆盖边界与中间情况：

lemma LemmaPowerDistribute(x: int, y: int)
    requires y >= 0
    ensures forall a :: 0 <= a <= y ==> power(x, y) == power(x, a) * power(x, y - a)
    decreases y
{
    if y == 0 {
        // 基础情况：仅a=0，利用power(x,0)=1直接验证
        assert power(x,0) == power(x,0) * power(x,0);
    } else {
        LemmaPowerDistribute(x, y-1); // 归纳假设：对y-1成立
        // 遍历所有a的取值范围验证
        forall a | 0 <= a <= y {
            if a == 0 || a == y {
                // 边界情况：利用power(x,0)=1直接验证
                assert power(x,y) == power(x,a) * power(x, y - a);
            } else {
                LemmaPowerStep(x, y-a); // 确保步长性质可用
                calc {
                    power(x, y);
                    == x * power(x, y-1); // 步长性质
                    == x * (power(x,a) * power(x, (y-1)-a)); // 归纳假设
                    == power(x,a) * (x * power(x, (y-a)-1)); // 代数交换律
                    == power(x,a) * power(x, y-a); // 步长性质
                }
            }
        }
    }
}

最终可验证代码 #

整合后的完整代码可正常通过Dafny验证：

function power(x: int, y: int) : int
    requires y >= 0
    ensures y == 0 ==> power(x,y) == 1
    ensures y > 0 && y % 2 == 0 ==> power(x,y) == power(x*x,y/2)
    ensures y > 0 && y % 2 == 1 ==> power(x,y) == x * power(x*x,(y-1)/2)
    decreases y
{
    if y == 0 then
        1
    else if y % 2 == 0 then
        power(x*x, y/2)
    else 
        (x * power(x*x,(y-1)/2))
}

// 证明幂函数步长性质
lemma LemmaPowerStep(x: int, y: int)
    requires y > 0
    ensures power(x, y) == x * power(x, y - 1)
    decreases y
{
    if y == 1 {
        assert power(x,1) == x * power(x,0);
    } else if y % 2 == 0 {
        let half = y/2;
        LemmaPowerStep(x*x, half);
        calc {
            power(x, y);
            == power(x*x, half);
            == (x*x) * power(x*x, half - 1);
            == x * (x * power(x*x, (y-2)/2));
            == x * power(x, y-1);
        }
    } else {
        let k = (y-1)/2;
        assert power(x, y-1) == power(x*x, k);
        calc {
            power(x, y);
            == x * power(x*x, k);
            == x * power(x, y-1);
        }
    }
}

// 证明幂函数分配律
lemma LemmaPowerDistribute(x: int, y: int)
    requires y >= 0
    ensures forall a :: 0 <= a <= y ==> power(x, y) == power(x, a) * power(x, y - a)
    decreases y
{
    if y == 0 {
        assert power(x,0) == power(x,0) * power(x,0);
    } else {
        LemmaPowerDistribute(x, y-1);
        forall a | 0 <= a <= y {
            if a == 0 || a == y {
                assert power(x,y) == power(x,a) * power(x, y - a);
            } else {
                LemmaPowerStep(x, y-a);
                calc {
                    power(x, y);
                    == x * power(x, y-1);
                    == x * (power(x,a) * power(x, (y-1)-a));
                    == power(x,a) * (x * power(x, (y-a)-1));
                    == power(x,a) * power(x, y-a);
                }
            }
        }
    }
}

// 统一验证额外性质（可选）
lemma VerifyPowerExtraProps(x: int, y: int)
    requires y >=0
    ensures y>0 ==> power(x,y) == x*power(x,y-1)
    ensures forall a ::0<=a<=y ==> power(x,y) == power(x,a)*power(x,y-a)
{
    if y>0 {
        LemmaPowerStep(x,y);
    }
    LemmaPowerDistribute(x,y);
}

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