Aptos Move Prover 測試套件完全指南基線測試、運(yùn)行指令與調(diào)試實(shí)踐【免費(fèi)下載鏈接】aptos-coreAptos is a layer 1 blockchain built to support the widespread use of blockchain through better technology and user experience.項(xiàng)目地址: https://gitcode.com/GitHub_Trending/ap/aptos-core本指南以 aptos-core 倉庫中 Move Prover 測試目錄third_party/move/move-prover/tests為核心系統(tǒng)講解其基于基線期望輸出baseline的單元測試機(jī)制如何配置驗(yàn)證工具鏈、如何運(yùn)行與更新測試、如何通過源碼內(nèi)指令directive與特性feature組合控制測試行為以及如何調(diào)試長時間運(yùn)行的驗(yàn)證用例。讀完本文你將能夠熟練地在本倉庫中運(yùn)行、新增和排查 Move Prover 的驗(yàn)證測試并理解其背后的驅(qū)動實(shí)現(xiàn)原理。Move Prover 測試目錄的定位與結(jié)構(gòu)Move Prover 是 Move 語言的形式化驗(yàn)證工具它把 Move 源碼編譯為無棧字節(jié)碼stackless bytecode再翻譯為 Boogie 中間表示并交給 Z3/cvc5 等 SMT 求解器從而證明或證偽函數(shù)上的規(guī)范spec。測試目錄tests存放的就是 Prover 的單元測試基線期望baseline expectation成功驗(yàn)證時 Prover 無輸出失敗驗(yàn)證時產(chǎn)生特定診斷信息這些診斷被存儲在.exp期望文件中測試驅(qū)動會逐字比對。測試輸入以.move源文件為主按目錄劃分測試域tests/sources/主單元測試目錄內(nèi)含functional/按功能組織如closures/、proof/、signed_int/、state_labels/、regression/回歸測試含.smt文件等子目錄tests/inference/端到端 spec 推斷spec inference測試每個用例把推斷生成的 Move 源碼與.exp.move基線比對見 inference_testsuite.rstests/xsources/擴(kuò)展測試extended tests默認(rèn)不運(yùn)行需要MVP_TEST_X1開啟內(nèi)含design/與timeout/等場景。除了本目錄的測試Prover 的穩(wěn)定性還依賴 Move 標(biāo)準(zhǔn)庫與 Diem/Aptos 框架的驗(yàn)證測試——它們通過 Move CLI 中的 Prover 集成在倉庫外部配置運(yùn)行并不在本目錄內(nèi)。注意本地運(yùn)行這些測試前必須安裝驗(yàn)證工具并設(shè)置環(huán)境變量詳見 安裝指南。如果配置 Prover 的環(huán)境變量未按要求設(shè)置本目錄所有測試都會平凡地通過源碼中表現(xiàn)為只生成 Boogie 文件、不真正驗(yàn)證見下文驅(qū)動實(shí)現(xiàn)一節(jié)。環(huán)境準(zhǔn)備安裝 Boogie、Z3 與 cvc5根據(jù) third_party/move/move-prover/doc/user/install.mdProver 依賴boogie、z3可選cvc5。在倉庫根目錄執(zhí)行./scripts/dev_setup.sh -yp . ~/.profile該命令適用于 macOS 與 LinuxUbuntu/CentOS 等Windows 暫不支持。它把工具安裝到用戶$HOME目錄并在~/.profile中寫入Z3_EXE、BOOGIE_EXE等環(huán)境變量定義若~/.profile未隨登錄 shell 自動加載需手動在~/.bash_profile中補(bǔ)充. ~/.profile。對于全新的開發(fā)機(jī)可一并安裝 Rust 等基礎(chǔ)構(gòu)建工具./scripts/dev_setup.sh -typ . ~/.profile遷移舊安裝的注意事項(xiàng)舊版安裝方式把 z3、dotnet、boogie 放在/usr/local/bin與/usr/local/share/dotnet需要 root 權(quán)限。若你的機(jī)器上仍存在公共位置的舊工具或自定義 .Net 安裝建議移除以避免版本不匹配尤其當(dāng)你要在命令行直接調(diào)用boogie、z3時同時刪除.bashrc中任何Z3_EXE、BOOGIE_EXE的舊定義因?yàn)檎_的新定義已由dev-setup.sh寫入~/.profile。從測試驅(qū)動的實(shí)現(xiàn)來看testsuite.rs當(dāng)BOOGIE_EXE為空、或在未使用 cvc5 時Z3_EXE為空使用 cvc5 時CVC5_EXE為空驅(qū)動會判定工具未配置此時將 Prover 設(shè)為generate_only只生成 Boogie 中間文件、不調(diào)用求解器并跳過基線比對——這正是文檔警告所有測試將平凡通過的源碼依據(jù)。直接調(diào)用 Prover 調(diào)試本目錄源碼本目錄中的源碼目前無法與 Move 包系統(tǒng)package system集成部分文件組合起來無法編譯因此調(diào)試時需要跳過包系統(tǒng)、直接調(diào)用 Prover。可以定義一個 shell 別名alias mvpcargo run -p move-prover -- --configmy_config.tomlmy_config.toml至少需要包含以下內(nèi)容language_version 2.2 # Or any other options move_deps [ /Users/you/aptos-core/third_party/move/move-stdlib/sources ] move_named_address_values [ std0x1, extensions0x2, ]其中move_deps聲明依賴的 Move 標(biāo)準(zhǔn)庫源碼路徑按你的實(shí)際倉庫路徑修改move_named_address_values為命名地址綁定值std0x1、extensions0x2。注意與舊版本不同當(dāng)前版本的 Prover不再通過MOVE_PROVER_CONFIG環(huán)境變量自動選擇配置文件必須顯式用--config指定。用 MVC_LOG 開啟調(diào)試日志Prover 的調(diào)試信息輸出到logcrate 的debug!通道日志配置與 Move 編譯器共享定義見 move-compiler-v2/src/logging.rs。MVC_LOGMove Compiler 的縮寫環(huán)境變量控制日志級別其格式為spec[file]MVC_LOG全部日志輸出到 stderrMVC_LOGinfo只輸出 info 及以上級別到控制臺MVC_LOGmodule_path_prefixinfo僅輸出匹配模塊如move_stackless_bytecode::function_target的 info 日志MVC_LOGfile或MVC_LOGinfofile寫入指定文件。注意環(huán)境變量只決定日志級別mvp別名還必須通過 verbose 標(biāo)志告知 Prover 產(chǎn)生debug!輸出。例如把編譯之后所有 Prover 階段的棧式字節(jié)碼stackless bytecode轉(zhuǎn)儲到prover.log用于針對性的 Prover 調(diào)試MVC_LOGmove_compiler_v2info,debugprover.log \ mvp --verbose debug --dump-bytecode enum_invariants.move運(yùn)行測試快速指南測試命令的完整快速指南如下重新生成基線文件UPBL1 cargo test 可選測試過濾條件UPBL 即 update baselines按特性收窄測試MVP_TEST_FEATUREfeature cargo test未設(shè)置時每個用例會按其啟用的所有特性分別測試特性的啟用機(jī)制見下文開啟一致性檢查MVP_TEST_INCONSISTENCY1 cargo test傳入自定義 Prover 標(biāo)志組合MVP_TEST_FLAGSflags cargo test改跑tests/xsources擴(kuò)展測試樹MVP_TEST_X1 cargo test。例如用 20 秒超時運(yùn)行全部測試MVP_TEST_FLAGS-T20 cargo test -p move-prover源碼內(nèi)測試指令directives測試源碼中的某些注釋會被測試驅(qū)動解釋為測試指令。指令的格式是源文件中的單行注釋// directive: value且可以重復(fù)出現(xiàn)。支持的指令如下指令作用// flag: flags在默認(rèn)標(biāo)志之外額外用給定標(biāo)志運(yùn)行該測試// no_ci:將該測試從 CI 運(yùn)行中排除// exclude_for: feature對包含式inclusive特性排除該測試// also_include_for: feature對排他式exclusive特性納入該測試倉庫中還能看到另一些驅(qū)動實(shí)際支持的指令例如// no-boogie-test:工具缺失時也跳過基線校驗(yàn)、// use-aptos-stdlib:改用 Aptos 標(biāo)準(zhǔn)庫路徑、// separate_baseline: feature為該特性單獨(dú)生成基線文件如 choice.move 中的// separate_baseline: cvc5以及// inference-output: file、// reject-incomplete-inference:、// inference-reject-mutation:等推斷類指令見 inference_testsuite.rs。指令的解析與提取由move_prover_test_utils::extract_test_directives完成并被 testsuite.rs 在收集用例時消費(fèi)。例如 aborts_if.move 是標(biāo)準(zhǔn)的功能測試源文件其對應(yīng)的 aborts_if.exp 記錄了諸如function does not abort under this condition、abort not covered by any of the aborts_if clauses等診斷信息。特性的包含模式特性feature分為兩類包含式inclusive默認(rèn)運(yùn)行全部測試除非用// exclude_for: feature顯式排除排他式exclusive只有帶// also_include_for: feature指令的測試才會運(yùn)行。README 中列出的特性有default以全部默認(rèn)標(biāo)志運(yùn)行測試no_opaque以忽略opaquepragma 的特殊模式運(yùn)行這會顯著增加 Prover 負(fù)載起到壓力測試stress test的作用cvc5運(yùn)行配置為使用 cvc5 求解器作為后端的測試。提示README 描述的是特性機(jī)制的一般形態(tài)。從當(dāng)前倉庫 testsuite.rs 的實(shí)現(xiàn)看實(shí)際注冊的特性為default隱式包含模式、在 CI 中啟用、無額外標(biāo)志與cvc5標(biāo)志為--use-cvc5隱式包含模式、暫不在 CI 啟用、且only_if_requestedtrue——只有顯式設(shè)置MVP_TEST_FEATUREcvc5才會運(yùn)行。源碼中以// exclude_for: cvc5排除的用例大量存在例如functional/下的位運(yùn)算與字節(jié)碼向量用例。在收集用例階段驅(qū)動會先按包含模式過濾testsuite.rs再在 CI 環(huán)境下MVP_TEST_ON_CI1檢查enable_in_ci與no_ci指令最后應(yīng)用特性的enabling_conditioncvc5 特性限定只作用于unit測試組。測試用例命名約定本目錄下的測試遵循統(tǒng)一的命名約定且一個文件內(nèi)可混合兩類用例正確性用例預(yù)期被 Prover 證明通過的正確 Move 函數(shù)反例用例預(yù)期被證偽的不正確 Move 函數(shù)其產(chǎn)生的錯誤存放在.exp期望基線文件中。按約定不正確的函數(shù)名帶_incorrect后綴例如abort2_incorrect、multi_abort3_incorrect并且預(yù)期只有帶此后綴函數(shù)的錯誤才會出現(xiàn)在.exp文件中。這為基線比對提供了可預(yù)測性如果.exp中出現(xiàn)了非_incorrect函數(shù)名的診斷通常意味著測試或規(guī)范本身出了問題。類似地inference測試以.exp.move保存推斷輸出的源碼基線inference_testsuite.rs 會依次執(zhí)行編譯模型 → 運(yùn)行 spec 推斷 → 在推斷結(jié)果上運(yùn)行 Prover → 比對.exp.move基線的完整流程。作為參考ModifiesTest.move 演示了模塊間modifies與opaque組合的規(guī)范寫法而 ModifiesErrorTest.move 則用mutate_at_test_incorrect這樣的命名表達(dá)預(yù)期失敗的用例。調(diào)試長時間運(yùn)行的測試Prover 默認(rèn)的超時時間為40 秒可通過-Tseconds標(biāo)志修改。健康的測試絕不應(yīng)該跑滿這么長時間為避免 CI 中的偶發(fā)不穩(wěn)定flake建議保證測試在-T20內(nèi)通過MVP_TEST_FLAGS-T20 cargo test -p move-prover另外測試驅(qū)動目前注釋掉了--num-instances2與--sequential等選項(xiàng)見 testsuite.rs原因是 Boogie 包裝器對超時的處理尚不完善、可能導(dǎo)致掛起如要定位長時間運(yùn)行的單個測試可以在驅(qū)動中打開被注釋的println!( testing {}, path...)并配合cargo test -- --test-threads1串行執(zhí)行。一致性檢查Inconsistency Check如果給定--check-inconsistency標(biāo)志Prover 除了驗(yàn)證目標(biāo)之外還會檢查驗(yàn)證假設(shè)中是否存在不一致inconsistent assumption。當(dāng)環(huán)境變量MVP_TEST_INCONSISTENCY1被設(shè)置時cargo test會在運(yùn)行sources下的測試時自動附加該標(biāo)志MVP_TEST_INCONSISTENCY1 cargo test -p move-prover在源碼層面MVP_TEST_FLAGS、MVP_TEST_X、MVP_TEST_FEATURE、MVP_TEST_ON_CI四個環(huán)境變量被定義為常量testsuite.rsMVP_TEST_FLAGS的內(nèi)容會被shell_words::split解析后追加到每個用例的標(biāo)志列表中testsuite.rs——這解釋了為什么通過該變量可以注入--check-inconsistency、-T20等任意 Prover 命令行參數(shù)。個別用例也會直接在源碼中通過// flag: --check-inconsistency開啟該檢查如functional/closures/下的部分測試。更新與新增測試的完整工作流結(jié)合以上機(jī)制總結(jié)在本倉庫中操作 Move Prover 測試的推薦流程確認(rèn)工具鏈按 安裝指南 安裝并導(dǎo)出BOOGIE_EXE、Z3_EXE需要時含CVC5_EXE新增用例在tests/sources/合適子目錄如functional/下新建.move文件遵循_incorrect后綴命名約定需要時附加// flag:、// exclude_for:、// no_ci:等指令生成基線運(yùn)行UPBL1 cargo test 新文件路徑片段生成.exp基線之后普通cargo test 文件片段即可比對收窄范圍使用MVP_TEST_FEATURE、MVP_TEST_FLAGS、MVP_TEST_X分別按特性、標(biāo)志組合與擴(kuò)展測試樹篩選穩(wěn)定性驗(yàn)證以MVP_TEST_FLAGS-T20 cargo test -p move-prover確認(rèn)用例不會拖慢 CI若涉及推斷流程則用tests/inference/下的.exp.move基線驗(yàn)證推斷輸出穩(wěn)定。這套基線比對 指令驅(qū)動 特性矩陣的設(shè)計使得 Move Prover 在持續(xù)集成中既能快速定位回歸任何輸出與.exp的差異都會失敗又能通過no_opaque、cvc5 等特性組合對求解器負(fù)載與后端兼容性做系統(tǒng)性壓力覆蓋是理解形式化驗(yàn)證工具工程質(zhì)量與測試哲學(xué)的一份高質(zhì)量參考實(shí)現(xiàn)?！久赓M(fèi)下載鏈接】aptos-coreAptos is a layer 1 blockchain built to support the widespread use of blockchain through better technology and user experience.項(xiàng)目地址: https://gitcode.com/GitHub_Trending/ap/aptos-core創(chuàng)作聲明：本文部分內(nèi)容由AI輔助生成（AIGC），僅供參考