Plutus项目中的Agda与Haskell评估器一致性测试问题分析

在Plutus智能合约开发平台中，Agda评估器与Haskell评估器之间的行为一致性是一个关键问题。本文深入探讨了在一致性测试过程中发现的一个重要技术挑战及其解决方案。

背景与问题发现

Plutus项目使用两种不同的评估器实现：一种是基于Haskell的实现，另一种是基于Agda的实现。为了确保两种实现的行为一致，项目组设计了一套一致性测试框架。这套框架能够比较两种评估器在相同输入下的输出结果，包括计算结果和执行预算消耗。

在测试过程中，开发团队发现Agda评估器在某些情况下（特别是涉及位运算内置函数时）产生的预算消耗与Haskell评估器不一致。这是由于Agda评估器尚未实现Haskell评估器中使用的特殊大小测量方法。

现有解决方案及其局限性

项目原本使用Test.Tasty.ExpectedFailure库中的expectFail函数来标记这些预期会失败的测试用例。这种方案有以下特点：

1. 测试运行时会明确显示哪些测试"预期失败"
2. 当Agda评估器被修复后，这些测试会开始通过，提醒开发人员更新测试配置

然而，这种方案存在一个严重问题：当使用--accept参数运行测试时，测试框架会错误地接受Agda评估器产生的不正确结果，并更新黄金文件（golden files）。黄金文件是包含预期结果的参考文件，用于验证测试输出是否正确。

替代方案评估

作为替代方案，开发团队考虑了使用ignoreTest函数：

1. 优点：使用--accept参数时不会错误地接受不正确的结果
2. 缺点：当Agda评估器被修复后，测试会继续保持"忽略"状态，可能导致开发人员忘记更新测试配置

技术决策与后续行动

经过分析，开发团队采取了以下行动：

1. 向Test.Tasty.ExpectedFailure库的维护者报告了这个问题
2. 在等待修复期间，考虑暂时切换到ignoreTest方案
3. 长期来看，需要完善Agda评估器的实现，确保其预算计算与Haskell评估器完全一致

这个问题不仅揭示了测试框架中的一个潜在缺陷，也反映了在实现形式化验证系统时保持与参考实现行为一致性的挑战。Plutus团队通过建立严格的一致性测试机制，确保了两种评估器实现的行为最终能够达成一致，为智能合约的安全执行提供了双重保障。