用Dafny正式验证Rust算法的九条规则（第二部分）

从验证 range-set-blaze Crate 中学到的教训

作者：Carl M. Kadie 和 Divyanshu Ranjan

这是一篇正式使用 Dafny 验证 Rust 算法的第二部分文章。我们将讨论规则 7 到 9：

• 7. 将真实的算法转换到 Dafny。
• 8. 验证你的算法的 Dafny 版本。
• 9. 重新修订你的验证以提高可靠性。

请参阅 第一部分 ，其中包含规则 1 到 6：

1. 不要学习 Dafny。
2. 学习 Dafny。
3. 定义你的算法的基本概念。
4. 指定你的算法。
5. 从 Dafny 社区寻求帮助。
6. 验证一个不同且更简单的算法。

这些规则基于我们验证来自于 “range-set-blaze” 的算法的经验，它是一个用于操作 “clumpy” 整数集合的 Rust crate。

回顾一下来自 第一部分 的规则 6 表明我们可以验证 “InternalAdd” 算法，但它不是 Rust crate 中使用的算法。我们接下来将转向该算法。

规则 7：将真实的算法转换到 Dafny

以下是感兴趣的 Rust 函数，其中一些代码暂时排除在外：

// https://stackoverflow.com/questions/49599833/how-to-find-next-smaller-key-in-btreemap-btreeset
// https://stackoverflow.com/questions/35663342/how-to-modify-partially-remove-a-range-from-a-btreemap
fn internal_add(&mut self, range: RangeInclusive<T>) {
    let (start, end) = range.clone().into_inner();
    assert!(
        end <= T::safe_max_value(),
        "end 必须小于等于 T::safe_max_value()"
    );
    if end < start {
        return;
    }
    //... 代码继续 ...
}

以下是 Dafny 的开始转换：

method InternalAdd(xs: seq<NeIntRange>, range: IntRange) returns (r: seq<NeIntRange>)
  requires ValidSeq(xs)
  ensures ValidSeq(r)
  ensures SeqToSet(r) == SeqToSet(xs) + RangeToSet(range){
  var (start, end) := range;
  if end < start {
    r := xs;
    return;
  }
  //... 代码继续 ...
}

可能有兴趣的几个要点：

• Rust 代码使用了 self 和面向对象的封装。Dafny 支持这种编码风格，但为了简单起见，我在这里没有使用它。具体而言，Rust 代码对 self 进行了变更。我选择在 Dafny 代码中更加函数式地编写它 —— 它接受一个不可变的序列并返回一个新的不可变的序列。
• Rust 代码使用借用检查器来管理内存。这导致了诸如 range.clone() 这样的表达式。Dafny 使用垃圾回收器来管理内存。在任一情况下，内存安全都会被处理。因此，在这个验证中我们忽略了它。
• Rust 代码对 T 进行了泛型定义，而我在其他地方将其定义为包括所有标准 Rust 整数类型（例如，u8，isize，i128）。Dafny 代码在 int 上进行了定义，它是一个代表任意大小整数的单一类型。这意味着这个 Dafny 转换不需要检查整数溢出。[请参阅之前的一篇文章，使用 Kani Rust 验证器对溢出安全性进行了正式证明。]
• Rust 代码包含一个运行时的 assert!，在 Rust 中需要用到它来禁止一种特殊情况：将 u128::max_value 插入到 RangeSetBlaze<u128>。由于 Dafny 使用任意大小的 int，它忽略了这种特殊情况。

补充：Rust的包容性范围0.. = u128 :: max_value的长度是多少？答案是u128 :: max_value+1，该值太大，无法用任何标准的Rust整数类型表示。 range-set-blaze包限制范围为0.. = u128 :: max_value -1，以便使用u128表示长度。

接下来让我们考虑internal_add算法的其余部分。请记住，我们有一些排序不相交范围的列表和一些非空的新范围，我们要插入该范围。例如

该算法要求我们查找位于新范围的起点（或者与之重叠）之前的（如果有）现有范围。将其称为“before”范围。然后我们考虑四种情况：

• 情况1：新范围不与其前置范围相接，因此我们在插入新范围的同时，检查它是否与其他范围相接。
• 情况2：新范围与前置范围相接且延伸至其之外，因此我们在检查它是否与其他范围相接的同时，延伸前置范围的末尾。（当没有其他范围相接时，这将非常快速。）

• 情况3：新范围与前置范围相接，但不延伸至其之外，因此不执行任何操作。（这将始终非常快速。）

• 情况4：新范围在任何范围之前开始，因此在检查它是否与其他范围相接的同时，将其添加进来。

这是Rust中的算法：

// 代码继续...// 未来：如果BTreeMap有一个返回两个迭代器的partition_point函数，则非常好    let mut before = self.btree_map.range_mut(..=start).rev();    if let Some((start_before, end_before)) = before.next() {        // 必须分两步检查，以避免溢出        if match (*end_before).checked_add(&T::one()) {            Some(end_before_succ) => end_before_succ < start,            None => false,        } {            self.internal_add2(&range);        } else if *end_before < end {            self.len += T::safe_len(&(*end_before..=end - T::one()));            *end_before = end;            let start_before = *start_before;            self.delete_extra(&(start_before..=end));        } else {            // 完全包含，所以不执行任何操作        }    } else {        self.internal_add2(&range);    }}

这是Dafny中的代码：

// 代码继续...  var beforeHi := IndexAtOrBeforePlusOne(xs, start);  if beforeHi > 0 { // 不在最前面    var (startBefore, endBefore) := xs[beforeHi-1];    if endBefore+1 < start {      r := InternalAdd2(xs, range);    } else if endBefore < end {      r := xs[..beforeHi-1] + [(startBefore, end)] + xs[beforeHi..];      assume exists i: nat :: i < |r| && r[i] == (startBefore,end) && ValidSeq(r[..i+1]) && ValidSeq(r[i+1..]);      r := DeleteExtra(r, (startBefore,end));    } else{      r := xs;    }  }  else // 在最前面  {    r := InternalAdd2(xs, range);  }}

可能感兴趣的一些要点：

• Rust代码通过键和值操作BTreeMap。Dafny代码通过（随机访问）索引操作排序的seq。尽管这使得Dafny代码不那么自然，但我让Dafny操作与Rust操作相匹配。
• Rust代码还更新self.len，即RangeSetBlaze中的个别整数的数量。Dafny代码忽略了这一点。（将len更新到Dafny代码中是一个可以在将来添加的功能。）
• 与以前一样，Rust版本包括避免溢出的代码，而Dafny则忽略了溢出问题。

我继续通过编写internal_add2和delete_extra的Dafny版本来进行移植，这两个函数是internal_add调用的。然后，我编写了这两个方法调用的方法，等等。完整的移植代码有大约185行。你可以在这里看到。

这个版本没有通过验证。下面我们来验证它。

规则8：验证Dafny版本的算法。

在这一步中，你将为你的代码添加验证提示，例如assert语句的形式。Dafny使用这些提示来尝试验证你的代码。作为一个Dafny新手，我（Carl）发现添加提示比编码更难。部分原因是因为我不知道（或者说不确定）Dafny是否满意，我可以停下来。

然而，我确实学到了应该如何开始。例如，上面的InternalAdd代码产生了两个验证错误。首先，Dafny验证器报告一个ensures可能不成立：

This postcondition might not hold: SeqToSet(r) == SeqToSet(xs) + RangeToSet(range)

旁注：“后置条件”对应ensures。“前置条件”对应requires。

其次，Dafny验证器抱怨DeleteExtra的前置条件（即其中之一的requires）无法证明。

我们将先专注于第一个问题，为方法的底部添加一个assert。我们将其写成与ensures相似的形式。

// ...在InternalAdd的最后一行添加这个assertassert SeqToSet(r) == SeqToSet(xs) + RangeToSet(range);}

我们暂时使用一个assume，来明确忽略DeleteExtra的问题。

// ...  assume exists i: nat :: i < |r| && r[i] == (startBefore,end) && ValidSeq(r[..i+1]) && ValidSeq(r[i+1..]);  r := DeleteExtra(r, (startBefore,end));//...

Dafny验证器现在只对我们新添加的最后一个assert抱怨。它说“可能不满足断言。”

回想一下，InternalAdd代码使用嵌套的if语句将其工作划分为五种情况。下一步，我们将其 assert 从方法的末尾移动到每个 case 的末尾。在结果中寻找以// case注释结尾的行：

method InternalAdd(xs: seq<NeIntRange>, range: IntRange) returns (r: seq<NeIntRange>)  requires ValidSeq(xs)  ensures ValidSeq(r)  ensures SeqToSet(r) == SeqToSet(xs) + RangeToSet(range){  var (start, end) := range;  if end < start {    r := xs;    assert SeqToSet(r) == SeqToSet(xs) + RangeToSet(range); // case 0 - 验证通过    return;  }  var beforeHi := IndexAtOrBeforePlusOne(xs, start);  if beforeHi > 0 { // 不从头插入    var (startBefore, endBefore) := xs[beforeHi-1];    if endBefore+1 < start {      r := InternalAdd2(xs, range);      assert SeqToSet(r) == SeqToSet(xs) + RangeToSet(range); // case 1 - 验证通过    } else if endBefore < end {      r := xs[..beforeHi-1] + [(startBefore, end)] + xs[beforeHi..];      assume exists i: nat :: i < |r| && r[i] == (startBefore,end) && ValidSeq(r[..i+1]) && ValidSeq(r[i+1..]);      r := DeleteExtra(r, (startBefore,end));      assert SeqToSet(r) == SeqToSet(xs) + RangeToSet(range); // case 2 - 验证失败    } else{      r := xs;      assert SeqToSet(r) == SeqToSet(xs) + RangeToSet(range); // case 3 - 验证失败    }  }  else // 从头插入  {    r := InternalAdd2(xs, range);    assert SeqToSet(r) == SeqToSet(xs) + RangeToSet(range); // case 4 - 验证通过  }}

Dafny现在告诉我们，0, 1,和4是有效的。案例2失败（并且包含我们最终需要删除的那个assume）。但是现在，让我们来处理案例3。

回想一下本文中第7条规则，案例3是指我们添加了一个新的范围（红色），该范围完全被现有范围（蓝色的“之前”范围）覆盖，所以代码不需要执行任何操作。

所以，从逻辑上思考，我们知道什么？我们知道被之前范围覆盖的整数是新范围覆盖的整数的超集。我们还知道之前范围是我们原始的排序并且不相交的范围列表（蓝色范围）的一部分。我们将这两个提示添加到我们的代码中，使用assert语句：

Dafny同意这两个提示是正确的（绿色勾号），但它仍然不接受感兴趣的assert（红色标记）。

我们似乎需要一个更多的提示。具体来说，我们需要说服Dafny之前范围覆盖的整数是所有排序和不相交范围列表的整数的子集。直观上讲，这是因为之前范围是列表中的一个范围。

我们将此提示编写为一个没有体的引理。Dafny接受了它。

使用引理，案例3现在是有效的：

这意味着我们已经验证了案例0, 1, 3和4。我们接下来将处理案例2。此外，一些提到的方法，例如DeleteExtra，还没有验证，我们需要在这些方法上工作。[您可以在此处查看到此刻的代码。]

有关验证调试的一般建议，请参考Dafny用户指南中的此部分。我还推荐Stack Overflow答案和James Wilcox教授的小教程。

总的来说，将验证算法的任务划分为许多较小的验证任务。我发现这比编程更困难，但不是太难，而且仍然有趣。

我最终为这185行常规代码添加了约200行验证代码（完整代码在此处）。当我最后验证完最后一个方法时，我错误地认为我已经完成了。

令我惊讶（并失望）的是，第一次验证一切并不能结束工作。您还必须确保您的项目将再次验证并对其他人进行验证。我们将在下一条规则中讨论这一点。

规则9：重新调整验证以提高可靠性。

我以为我完成了。然后，我将数学Min函数的六行定义从Dafny标准库移动到了我的代码中。这导致我的验证失败，没有逻辑原因（确实如此！）。后来，在我以为我已经修复了它之后，我删除了一个未使用的方法。同样，验证开始无缘无故地失败。

发生了什么？Dafny通过随机搜索的启发式方法工作。表面上改变代码（或改变随机种子）会改变搜索所需的时间量。有时，计算时间会发生剧变。如果新时间超过用户设置的时间限制，验证将失败。[我们将在下面的第3个技巧中详细讨论时间限制。]

您应该通过尝试不同的随机种子来测试您的验证的可靠性。这是我在 Windows 上验证文件时使用的命令，使用了 10 个随机种子。

@rem 找到 Dafny 的位置并将其添加到您的路径中set path=C:\Users\carlk\.vscode-insiders\extensions\dafny-lang.ide-vscode-3.1.2\out\resources\4.2.0\github\dafny;%path%dafny verify seq_of_sets_example7.dfy --verification-time-limit:30 --cores:20 --log-format csv --boogie -randomSeedIterations:10

结果是一个 *.csv 文件，您可以将其作为电子表格打开，然后查找故障：

另外：有关测量 Dafny 验证可靠性的更多想法，请参阅此关于分析 *.csv 文件的 Stack Overflow 答案和此推荐使用 dafny-reportgenerator 工具的 GitHub 讨论。

在找到问题点后，我请来了共同作者 Divyanshu Ranjan 来提供帮助。Divyanshu Ranjan 利用他在 Dafny 上的经验解决了该项目的验证问题。

以下是他的建议，结合项目示例：

Tip #1：在可能的情况下，删除涉及“forall”和“exists”的 require 语句。

回顾一下规则 4，幽灵函数 SeqToSet 返回由排序的不相交非空范围列表覆盖的整数集。我们通过函数 ValidSeq 来定义“排序的不相交”，其中内部使用了两个 forall 表达式。我们可以删除列表必须排序且不相交的要求，如下所示：

ghost function SeqToSet(sequence: seq<NeIntRange>): set<int>  decreases |sequence|  // removed: requires ValidSeq(sequence){  if |sequence| == 0 then {}  else if |sequence| == 1 then RangeToSet(sequence[0])  else RangeToSet(sequence[0]) + SeqToSet(sequence[1..])}

从我们的角度来看，我们有相同的有用函数。从 Dafny 的角度来看，这个函数避免了两个 forall 表达式，并且更容易应用。

Tip #2：使用 calc 来避免 Dafny 的猜测工作。

通过 Dafny 的 calc 语句，您列出了到达结论所需的确切步骤。例如，这是 DeleteExtra 方法中的一个 calc：

calc {    SeqToSet(xs[..indexAfter+1]) + SeqToSet(xs[indexAfter+1..]);  ==    { SeqToSetConcatLemma(xs[..indexAfter+1], xs[indexAfter+1..]); }    SeqToSet(xs[..indexAfter+1] + xs[indexAfter+1..]);  ==    { assert xs == xs[..indexAfter+1] + xs[indexAfter+1..]; }    SeqToSet(xs);  ==    { SetsEqualLemma(xs, r[indexAfter], r2, indexAfter, indexDel); }    SeqToSet(r2);  }

在代码的这一点上，xs 是一个范围序列，但它可能不是排序的也不是不相交的。这个 calc 断言：

1. 由 xs 的两个部分覆盖的整数，等于
2. 由其两个部分的连接覆盖的整数，等于
3. 由 xs 覆盖的整数，等于
4. rs。

对于每个步骤，我们可以包含引理或断言来帮助证明该步骤。例如，这个断言有助于证明从第 3 步到第 4 步的转变：

{ 假设 xs == xs[..indexAfter+1] + xs[indexAfter+1..]; }

为了效率和控制，这些引理和断言不会在验证器的步骤之外可见。这保持了Dafny的专注。

提示 #3：使用timeLimit在需要时提供计算。

Dafny在达到用户设定的timeLimit时停止尝试验证方法。通常使用10、15或30秒的限制，因为作为用户，我们通常希望永远不会发生的验证迅速失败。然而，如果我们知道验证最终会发生，我们可以设置一个方法特定的时间限制。例如，Divyanshu Ranjan注意到DeleteExtra通常确实可以验证，但比其他方法需要更多时间，因此他添加了一个方法特定的时间限制：

method {:timeLimit 30} DeleteExtra(xs: seq<NeIntRange>, internalRange: IntRange) returns (r: seq<NeIntRange>)// ...

另外：由于timeLimit不考虑不同计算机的速度差异，因此请设置得稍微大一点。

提示 #4：使用split_here将一个验证问题分成两部分。

如Dafny FAQs所解释的那样，有时将一组断言一起验证比逐个验证更快。

使用assert {:split_here} true;语句将一系列断言分成两部分进行验证。例如，即使使用了timeLimit，DeleteExtra也会超时，直到Divyanshu Ranjan添加了以下内容：

// ...else  {    r := (s[..i] + [pair]) + s[i..];    assert r[..(i+1)] == s[..i] + [pair];    assert r[(i+1)..] == s[i..];    assert {:split_here} true; // 将验证分为两个部分    calc {      SeqToSet(r[..(i+1)]) + SeqToSet(r[(i+1)..]);// ...

提示 #5：保持引理简洁。如果需要，将保证跨引理分割。

有时引理试图一次做太多事情。考虑SetsEqualLemma。它与删除冗余区间有关。例如，如果我们将a插入xs，则标记为“X”的区间变得冗余。

SetsEqualLemma的原始版本包含12个requires和3个ensures。Divyanshu Ranjan将其拆分为两个引理：RDoesntTouchLemma（11个requires和2个ensures）和SetsEqualLemma（3个requires和1个ensures）。通过这个改变，项目的验证变得更加可靠。

应用这些提示将提高我们证明的可靠性。我们能使验证100%可靠吗？可悲的是，不能。总有一种可能性，即在不幸的情况下，Dafny无法验证。那么，何时停止尝试改进验证呢？

在这个项目中，Divyanshu Ranjan和我不断改进验证代码，直到任何单独运行的验证错误机率降低到33%以下。因此，在10次随机运行中，我们没有看到超过2或3个失败。我们甚至尝试了100次随机运行。进行100次运行时，我们看到30个失败。

结论

所以，这就是使用Dafny证明Rust算法正确性的九个规则。也许你会对这个过程不那么容易或自动感到沮丧。然而，我对这个过程本身的可能性感到鼓舞。

旁白：自从高中几何课上以来，我就觉得数学证明既迷人又令人沮丧。它让我感到“迷人”的原因是一旦证明了一个数学定理，它就永远被认为是真实的（欧几里得几何仍然被认为是真实的，而亚里士多德的物理学不是）。而让我感到“沮丧”的原因是我的数学课似乎总是模糊不清地告诉我可以假设哪些公理以及我的证明可以走多大的步骤。Dafny和类似的系统通过自动证明检查消除了这种模糊性。在我的观点看来，更好的是，它们帮助我们创建关于我深深关注的领域（算法）的证明。

何时值得对算法进行正式证明？考虑到所涉及的工作，我只会在以下情况下再次这样做：算法具有一些棘手、重要或易于证明的组合。

未来该过程可能如何改进？我希望看到以下几点：

• 系统之间的互换——一旦证明了一个几何定理，就不再需要再次证明。如果检查算法证明的系统可以使用彼此的证明，那就太好了。
• 像 Dafny 一样易于使用的全 Rust 系统——有关这方面的工作，请参见[1,2]。

旁白：您知道有没有一个易于使用的 Rust 验证系统？请考虑将其应用于 internal_add 的验证。这将使我们能够比较 Rust 系统的易用性和功能与 Dafny 的。

• Rust 版的证明类似于 Cargo.lock 文件—— 在 Rust 中，我们使用 Cargo.lock 来锁定一个已知好的项目依赖组合。我希望当 Dafny 找到一种方式证明了一个方法时，它能够锁定它所找到的证明步骤。这可以使验证更可靠。
• 更好的验证人工智能—— 我的直觉是，稍微改进一下 ChatGPT，它可能擅长创建所需验证代码的90%。我发现当前的 ChatGPT 4 在处理 Dafny 时表现不佳，我认为是因为缺乏 Dafny 的训练示例。
• 为人工智能提供更好的验证——当人工智能生成代码时，我们担心代码的正确性。正式验证可以通过证明正确性来帮助解决这个问题（有关这方面的一个小例子，请参见我的文章 “完全自动检查人工智能生成代码”）。

感谢您加入我们的程序正确性之旅。我们希望如果您有一个需要证明的算法，这些步骤将帮助您找到相应的证明。

请关注 VoAGI 上的 Carl。我在 Rust 和 Python 的科学编程、机器学习和统计方面进行写作。我倾向于每月发布一篇文章。

在<a href=”/?s=他的博客上阅读更多 Divyanshu Ranjan 的作品</a>。除了正式方法之外，博客还涉及几何、统计学等内容。