Dafny中定义映射与函数的满射谓词遇验证问题

问题背景 #

我在Dafny中定义映射与函数的满射谓词时遇到了验证问题，已编写的谓词定义代码如下：

predicate isTotal<G(!new), B(!new)>(f:G -> B)
    reads f.reads;
{
     forall g:G :: f.requires(g)
}

predicate Surjective<A(!new), B(!new)>(f: A -> B) 
    requires isTotal(f)
{
    forall b: B :: exists a: A :: f(a) == b 
}

predicate isTotalMap<G(!new), B(!new)>(m:map<G,B>)
{
     forall g:G :: g in m
}

predicate mapSurjective<U(!new), V(!new)>(m: map<U,V>)
    requires forall u: U :: u in m.Keys
{
    forall x: V :: exists a: U :: m[a] == x
}

测试有限枚举类型Color的函数与映射时，多个断言无法通过验证，测试代码如下：

datatype Color = Blue | Yellow | Green | Red

function toRed(x: Color): Color {
    Red
}

function shiftColor(x: Color): Color {
    match x {
        case Red => Blue
        case Blue => Yellow
        case Yellow => Green
        case Green => Red
    }
}

lemma TestSurjective() {
    assert isTotal(toRed);
    assert isTotal(shiftColor);
    var toRedm := map[Red := Red, Blue := Red, Yellow := Red, Green := Red];
    var toShiftm := map[Red := Blue, Blue := Yellow, Yellow := Green, Green := Red];
    // assert Surjective(toRed); //should fail
    // assert Surjective(shiftColor); //should succeed
    // assert mapSurjective(toRedm); //should fail
    // assert forall u: Color :: u in toShiftm.Keys;
    assert isTotalMap(toShiftm); //also fails
    assume forall u: Color :: u in toShiftm.Keys;
    assert mapSurjective(toShiftm); // should succeed
}

具体问题 #

• 映射无法满足mapSurjective中的totality要求，推测是因为映射可能是堆对象，Dafny未跟踪其内容，但即使假设前置条件，对应的满射断言仍不通过；
• 有限类型的shiftColor函数的Surjective断言失败，对于无限类型我能理解，但有限类型应该可以完成验证，希望得到解答。

解决方案 #

问题1：映射的totality与满射验证

Dafny的map类型不会自动推断所有枚举键都存在，需要显式告知验证器映射的完整性：

1. 验证映射完整性：针对isTotalMap(toShiftm)，可以逐个验证枚举值是否在映射中：

   assert Red in toShiftm;
   assert Blue in toShiftm;
   assert Yellow in toShiftm;
   assert Green in toShiftm;
   assert isTotalMap(toShiftm); // 此时断言可通过
   

2. 验证映射满射：即使假设了totality，Dafny需要显式的存在性证明，针对每个Color值找到对应的原像：

   assume forall u: Color :: u in toShiftm.Keys;
   // 显式证明每个Color都有对应的原像
   assert exists a: Color :: toShiftm[a] == Red; // Green对应Red
   assert exists a: Color :: toShiftm[a] == Blue; // Red对应Blue
   assert exists a: Color :: toShiftm[a] == Yellow; // Blue对应Yellow
   assert exists a: Color :: toShiftm[a] == Green; // Yellow对应Green
   assert mapSurjective(toShiftm); // 此时断言可通过
   

问题2：有限类型函数的满射验证

shiftColor是循环置换函数，本身是满射的，但Dafny不会自动枚举所有情况验证，需要显式证明每个Color值都有原像：

lemma shiftColorIsSurjective()
    ensures Surjective(shiftColor)
{
    // 逐个证明每个Color都存在对应的输入
    assert exists x: Color :: shiftColor(x) == Red; // Green
    assert exists x: Color :: shiftColor(x) == Blue; // Red
    assert exists x: Color :: shiftColor(x) == Yellow; // Blue
    assert exists x: Color :: shiftColor(x) == Green; // Yellow
}

在TestSurjective中调用该引理后，即可通过断言：

lemma TestSurjective() {
    assert isTotal(toRed);
    assert isTotal(shiftColor);
    shiftColorIsSurjective();
    assert Surjective(shiftColor); // 现在断言可通过
    // ... 其他代码
}

另外，Surjective(toRed)会按预期失败，因为它始终返回Red，无法覆盖所有Color值，无需额外处理。

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