Verus语言中choose表达式返回元组的类型推导优化

在形式化验证工具Verus的开发过程中，我们发现了一个关于choose表达式类型推导的有趣问题。choose是Verus提供的一个强大功能，允许开发者从满足特定条件的值中选择一个实例，这在形式化验证中非常有用。

问题背景

在Verus的文档示例中，展示了如何使用choose表达式来选择满足less_than条件的整数对：

spec fn less_than(x: int, y: int) -> bool {
    x < y
}

proof fn test_choose_succeeds2() {
    assert(less_than(3, 7));
    let (x, y): (int, int) = choose|i: int, j: int| less_than(i, j);
    assert(x < y);
}

当前实现中，开发者需要显式地为元组(x, y)添加类型注解: (int, int)，这增加了代码冗余。理想情况下，Verus应该能够自动推导出这个类型信息。

技术分析

choose表达式在Verus中扮演着重要角色，它允许从满足给定谓词的值中选择实例。在这个例子中，我们选择的是两个整数i和j，它们满足i < j的关系。

类型推导问题出现在元组解构时。Verus目前无法自动推导出choose返回的元组类型，尽管从上下文可以清楚地看出：

1. less_than函数的参数类型明确为int
2. choose绑定的变量i和j也显式声明为int类型
3. 返回的元组(x, y)显然应该与(i, j)类型相同

解决方案

要解决这个问题，我们需要增强Verus的类型推导能力，特别是在处理choose表达式返回的元组时。具体来说：

1. 编译器应该利用choose绑定的变量类型信息
2. 当元组模式匹配与choose结合时，应该自动传播类型信息
3. 保持与Rust一致的类型推导行为，确保一致性

实现这一改进后，开发者可以简化为：

let (x, y) = choose|i: int, j: int| less_than(i, j);

影响与意义

这一改进虽然看似微小，但对于Verus的用户体验有显著提升：

1. 减少样板代码，使验证代码更加简洁
2. 保持类型安全的同时提高开发效率
3. 使Verus的类型推导更加智能，接近现代编程语言的期望

对于形式化验证工具而言，这类改进有助于降低入门门槛，让开发者更专注于验证逻辑本身而非语法细节。

总结

Verus团队已经解决了这个问题，移除了文档中的TODO注释。这一改进体现了Verus持续优化用户体验的承诺，也展示了形式化验证工具在保持严谨性的同时追求开发便利性的平衡艺术。