Move Prover 的 CVC4 后端集成指南：求解器切换、测试基线与编码定制

Move Prover 的 CVC4 后端集成指南求解器切换、测试基线与编码定制【免费下载链接】diemDiem’s mission is to build a trusted and innovative financial network that empowers people and businesses around the world.项目地址: https://gitcode.com/gh_mirrors/di/diemCVC4 集成是 Move Prover 中一项仍在演进的实验性功能本文面向工具开发者系统讲解如何在当前 Diem 仓库的 Move Prover 中把 CVC4 用作后端求解器、如何通过测试套件验证 CVC4 路径的正确性、如何导出并分析 smtlib 中间产物以及如何借助 Tera 模板系统为 CVC4 定制 Boogie 编码尤其是可替换的向量理论。读完本文你将掌握从--use-cvc4一行命令到深入修改验证编码的完整工作流。一、CVC4 集成概览Move Prover 的典型验证链路是Move 源码 → 带规范spec的 Boogie 中间表示 → 后端 SMT 求解器默认是 Z3。CVC4 作为可选的 SMT 求解器后端通过 Boogie 的-proverOpt:SOLVERcvc4机制接入。从当前仓库源码看该集成还处于早期阶段在 testsuite.rs 中cvc4测试组明确标注enable_in_ci: false暂不在 CI 中运行其注释说明这是 an experimental feature which is still evolving。本文默认读者已按用户文档配置好mvp命令行例如在.bashrc中设置alias mvpcargo run --release --quiet --package move-prover --后续所有命令均以mvp arguments形式给出。二、选择 CVC4 作为后端求解器2.1 基本用法切换到 CVC4 后端只需一个命令行开关# mvp --use-cvc4 source.move该开关对应BoogieOptions.use_cvc4见 options.rs。当use_cvc4为真时Boogie 命令行会追加-proverOpt:SOLVERcvc4 -proverOpt:PROVER_PATHCVC4_EXE 的值否则默认情况追加的是-proverOpt:PROVER_PATHZ3_EXE 的值。也就是说--use-cvc4与--z3-exe/--cvc4-exe两个路径选项是配合使用的。2.2 通过配置文件与环境变量管理求解器路径在 options.rs 的Default实现中三个关键可执行文件路径均从环境变量读取boogie_exe←BOOGIE_EXEz3_exe←Z3_EXEcvc4_exe←CVC4_EXE因此最省事的做法是把环境变量与~/.mvprc配置一起设置。~/.mvprc是 prover 的默认配置文件用户文档prover-guide.md展示了如何用它指向当前分支的 Move 标准库与 Diem framework# 配置默认依赖路径指向本地 Diem 分支 echo move_deps [\path-to-diem/language/diem-framework/modules\] ~/.mvprc export MOVE_PROVER_CONFIG~/.mvprc # 配置三个后端可执行文件 export BOOGIE_EXEpath-to-boogie/boogie export Z3_EXEpath-to-z3/z3 export CVC4_EXEpath-to-cvc4/cvc4配置文件与命令行是同一套选项系统的两种入口所有命令行选项以及更多选项都可以写进 toml 配置文件用mvp --print-config可以打印全部可用选项的 toml 模板作为自定义配置的蓝本。注意 toml 中[backend]一节即对应BoogieOptions。2.3 工具版本校验BoogieOptions::check_tool_versions()options.rs会在 prover 启动时校验各工具版本Boogie 版本必须不低于2.9.0MIN_BOOGIE_VERSION使用 Z3 时Z3 版本必须不低于4.8.9MIN_Z3_VERSION使用 CVC4 时通过cvc4 --version输出中git master ([0-9a-f]*)捕获 git hash并要求与EXPECTED_CVC4_VERSION aac53f51完全一致——也就是说当前仓库的 CVC4 集成针对特定 git 提交的 CVC4 构建验证过使用其他版本会报错 expected git hash aac53f51 but found ... forcvc4。这与文档中CVC4 集成仍是实验性、仍在演进的定位一致。2.4 默认 Boogie 参数无论选择哪个求解器prover 都会附加一组默认 Boogie 参数DEFAULT_BOOGIE_FLAGS-doModSetAnalysis -printVerifiedProceduresCount:0 -printModel:1 -enhancedErrorMessages:1 -monomorphize其中-monomorphize与后文完全单态化fully monomorphized的验证条件传递方式直接相关。三、使用 CVC4 运行测试3.1 测试套件的 feature group 机制prover 的测试套件入口为 testsuite.rs支持多个feature groups每个 group 代表一组以特定配置运行的测试。在 prover crate 中执行cargo test时默认会运行所有 group文档原话whencargo testis executed in the prover crate, all groups are executed。当前仓库注册了三个 feature见 testsuite.rs 的get_features()feature附加 flags包含模式是否进 CI说明default无Implicit隐式默认全含是使用 Z3 与默认配置no_opaque--ignore-pragma-opaque-internal-onlyImplicit是忽略内部函数的 opaque pragmacvc4--use-cvc4Implicit否enable_in_ci: false以 CVC4 作为 Boogie 后端对于cvc4组其enabling_condition为|group, _| group unit即只有move-prover/tests中的单元测试被纳入Diem framework 测试group 为diem与 move-stdlib 测试group 为stdlib被跳过——这正是文档所述Diem framework tests are skipped的源码依据。另外文档提到这些测试only run locally and nightly, but not in CI对应源码中的enable_in_ci: false以及collect_enabled_tests中在MVP_TEST_ON_CI1环境下对feature.enable_in_ci的检查逻辑。3.2 聚焦运行某个 feature group开发时往往只关心特定 group使用环境变量MVP_TEST_FEATURE即可收窄MVP_TEST_FEATUREcvc4 cargo test测试驱动还支持若干写在 Move 测试源文件里的指令directive形式为单行注释// directive: value详见 tests/README.md// flag: flags在本测试默认 flags 基础上附加运行参数// no_ci:将该测试从 CI 中排除// exclude_for: feature把测试从某个包含式inclusivefeature 中排除// also_include_for: feature把测试纳入某个排他式exclusivefeature// separate_baseline: feature为某 feature 单独维护基线文件见下。其他常用测试环境变量包括MVP_TEST_FLAGS附加任意 flags 组合、MVP_TEST_INCONSISTENCY1启用不一致性检查、MVP_TEST_X1改跑tests/xsources树。3.3 基线baseline约定测试属于基线测试baseline testsprover 的预期输出存储在.exp文件中。关于 CVC4 组的基线仓库与文档保持一致的三条规则默认共享基线默认情况下cvc4组与使用 Z3 的default组共享同一个.exp文件即期望 CVC4 与 Z3 在这些用例上给出相同判定。独立基线部分测试在源码中标注// separate_baseline: cvc4它们拥有独立的基线文件。get_flags_and_baseline()中独立基线的文件名格式为源文件名.cvc4_exp将扩展名替换为{feature}_exp。这些用例代表两类情况大多数是 CVC4 产生误报false positive的已知问题少数是模型选择差异导致的合法输出差异。基线更新用UPBL1 cargo test重新生成基线想只更新或只跑单个文件可在命令后附加 Move 源路径片段作为过滤。仓库中实际标注// separate_baseline: cvc4的测试包括 choice.moveCVC4 对部分 choice 产生误报、emits.move大多数验证问题的误报、hash_model.move、invariants_resources.move 等文件头部的// TODO(cvc4): ...注释直观记录了这些已知问题。一个实用的健壮性检查默认每 VC 超时为 40 秒vc_timeout可用-Tseconds调整为保证 CI 稳定建议测试在-T20下也能通过即MVP_TEST_FLAGS-T20 cargo test -p move-prover见 tests/README.md。四、获取 Boogie 生成的 smtlib 文件当需要脱离 Move 层、直接在 SMT 层面分析某个验证问题时可以用如下命令导出 Boogie 传递给求解器的 smtlib 输入# mvp --generate-smt [ --verify-only function-name ] source.move--generate-smt对应BoogieOptions.generate_smt为真时 Boogie 命令行追加-proverLog:PROC.smt--verify-only function-name用于把验证限定到单个函数该命令会为 Move 源码中的每个函数生成一个以.smt结尾的文件文件名取自被验证函数。文档特别强调这些 smtlib 文件的内容是hermetic封闭自足的上游prover/Boogie传递给求解器的所有设置包括求解器选项、量化器实例化阈值等都固化在文件内因此可以用该文件离线复现求解器行为而无需再依赖 prover 环境。这与用户文档中-C backend.generate_smttrue的等价说明一致prover-guide.md。五、为 CVC4 特化 Boogie 编码5.1 Tera 模板系统与根模板prover 生成 Boogie 源码的核心是 [Tera] 模板系统——它提供条件判断与宏展开能力语法与 Django2 类似、易于理解且表达力较强。每个验证问题都会包含的根模板位于 prelude.bpl它本身是模板化的 Boogie 源码会继续 include 其他模板例如向量vector与多重集multiset的理论模板Move 原生类型实现位于 native.bpl。模板的实际渲染发生在 boogie-backend/src/lib.rs 的add_prelude()它通过include_bytes!把上述.bpl模板编译进二进制注册进Tera::default()再以Context注入options即BoogieOptions、vec_instances单态化后的VecT实例集合以及 BCS/Event 原生类型的实例集合最后渲染出完整 prelude。其中-monomorphize标志保证到达 SMT 后端的验证条件VC是完全单态化的。5.2 在模板中访问后端选项在模板内部可以直接访问 prover 的[backend]配置节即BoogieOptions的所有字段。判断当前是否选择了 CVC4{% if options.use_cvc4 %} ... {% endif %}即模板表达式{{options.use_cvc4}}。新增选项只需在 Rust 的BoogieOptions中添加字段options.rs即可自动通过 Tera context 暴露给模板使用——模板中的{{options.字段名}}直接对应BoogieOptions的同名字段。5.3 替换向量理论Vector Theoriesprover 结合 Rust 代码与模板支持多种向量理论通过选项--vector-theory选择。当前仓库中VectorTheory枚举options.rs定义了五种与 prelude 下的理论文件一一对应枚举项对应模板文件是否外延is_extensionalBoogieArrayvector-array-theory.bpl否默认理论BoogieArrayInternvector-array-intern-theory.bpl是SmtArrayvector-smt-array-theory.bpl否SmtArrayExtvector-smt-array-ext-theory.bpl是SmtSeqvector-smt-seq-theory.bpl是is_extensional()告知 prover 该理论是否支持在元素支持的前提下外延相等。derive_options()会根据所选理论联动派生其他选项例如选SmtArray/SmtArrayExt时自动开启use_array_theory并相应追加-useArrayTheorySmtArray还会追加/proverOpt:O:smt.array.extensionalfalse外延性理论会启用native_equality。以默认的 vector-array-theory.bpl 为例它声明了{:datatype} Vec _与构造器VecT(v: [int]T, l: int)并实现了一组函数EmptyVec、MakeVec1..4、ExtendVec、ReadVec、LenVec、IsEmptyVec、RemoveVec、RemoveAtVec等——任何新增的向量理论都必须实现与这组函数相同的函数集合才能被 prover 其他代码字节码翻译器等正常使用。新增一个 CVC4 专用向量理论的完整步骤如下文档给出、并有源码印证编写理论以 vector-array-theory.bpl 为起点编写新的.bpl模板实现同样的函数接口扩展枚举在 options.rs 的VectorTheory枚举中增加一个条目同时记得在紧邻的is_extensional()中为新理论返回恰当的值——该返回值决定 prover 是否认为理论支持外延相等接线到 boogie-backend/src/lib.rs 中仿照其他理论的模式在add_prelude()的match options.vector_theory里把新模板绑定为vector-theory并把它加入include_bytes!常量。完成后即可通过--vector-theoryMyEnumItemName使用新理论。单态化注意事项这些理论运行在 Boogie 的monomorphization模式下。对于类型Vec T实际到达 SMT 后端的具体类型形如Vec_2923Vec的某个实例化。一般而言到达 SMT 后端的 VC 都是完全单态化的——要么经由 Boogie 的机制要么经由 Move prover 模板与代码生成中的显式逻辑vec_instances的收集就是后者的体现。六、基准测试与结果分析Move prover 自带一套支持系统化基准测试的工具与约定位于 move-prover/labcrate 名prover-labRust CLI 由cargo run -p prover-lab调用提供benchmark.rs、plot.rs、z3log.rs等模块可生成按模块mod_by_mod与按函数fun_by_fun的对比图表。CVC 对比实验仓库中已有 lab/data/cvc 目录其 README 说明该 lab 用于比较 cvc4README 中写作 cvc5与 z3对比范围是完整 Diem frameworkprover 的 cvc4/z3 配置存放在experiments/*.toml采用用户指南中标准的 Move prover 选项文件格式当前只对比非外延、基于 boogie-array的基础向量理论。run.sh运行基准并更新experiments/*下的数据文件plot.sh把结果转为本目录下的.svg。向量理论基准lab/data/vector-theories 对上述五种向量理论做模块/函数级验证时间对比可直接作为为新向量理论建 lab的模板。原文档的 TODO 与扩展方向原文档计划在 CVC4 集成通过单元测试后以lab/data/new-boogie为起点新建lab/data/z3-cvc4对比实验该计划在仓库中已部分落地为上述lab/data/cvc。七、小结CVC4 集成的当前状态与使用建议综合文档与仓库源码当前 CVC4 集成的状态可以概括为使用层面一条mvp --use-cvc4 source.move即可切换后端配合CVC4_EXE环境变量与~/.mvprc配置即可在本地复现注意 CVC4 的 git hash 必须为aac53f51见 options.rs 的版本校验。质量保障层面cvc4测试组默认共享 Z3 的.exp基线只有标注// separate_baseline: cvc4的用例才使用独立基线多为已知误报且该组目前不进 CI、只覆盖tests单元测试——使用时要对误报保持预期。工程调试层面--generate-smt导出的 hermetic smtlib 文件与output.bpl/output.bpl.log默认产物是分析求解器行为的利器。扩展层面Tera 模板 BoogieOptions字段 VectorTheory枚举 add_prelude()接线构成了一条清晰的自定义编码/理论扩展路径。适用前提与限制以上行为以当前仓库快照language/move-prover目录为准CVC4 集成属于实验特性版本校验严格、CI 未覆盖、存在已知误报生产级使用前应结合-Tseconds超时设置与本地 nightly 测试结果自行评估。延伸阅读完整的 prover 用户指南见 prover-guide.md安装与工具配置见 install.md测试驱动指令与基线约定见 tests/README.md测试组配置实现见 testsuite.rs。【免费下载链接】diemDiem’s mission is to build a trusted and innovative financial network that empowers people and businesses around the world.项目地址: https://gitcode.com/gh_mirrors/di/diem创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考