prove

Proves a Move Package

This is a tool for formal verification of a Move package using the Move prover.

Usage

movement aptos move prove [OPTIONS]

Options

• --dev Enables dev mode, which uses all dev-addresses and dev-dependencies. Dev mode allows for changing dependencies and addresses to the preset [dev-addresses] and [dev-dependencies] fields. This works both inside and out of tests for using preset values. Currently, it also additionally pulls in all test compilation artifacts.

• --package-dir <PACKAGE_DIR> Path to a move package (the folder with a Move.toml file).

• --output-dir <OUTPUT_DIR> Path to save the compiled move package. Defaults to <package_dir>/build.

• --named-addresses <NAMED_ADDRESSES> Named addresses for the move binary. Example: alice=0x1234, bob=0x5678. Note: This will fail if there are duplicates in the Move.toml file remove those first. [default: ]

• --skip-fetch-latest-git-deps Skip pulling the latest git dependencies. This will allow overriding this for local development.

• --bytecode-version <BYTECODE_VERSION> Specify the version of the bytecode the compiler is going to emit.

• -v, --verbosity <VERBOSITY> Verbosity level.

• -f, --filter <FILTER> Filters targets out from the package. Any module with a matching file name will be a target, similar as with cargo test.

• -t, --trace Whether to display additional information in error reports. This may help debugging but also can make verification slower.

• --cvc5 Whether to use cvc5 as the smt solver backend. The environment variable CVC5_EXE should point to the binary.

• --stratification-depth <STRATIFICATION_DEPTH> The depth until which stratified functions are expanded. [default: 6]

• --random-seed <RANDOM_SEED> A seed for the prover. [default: 0]

• --proc-cores <PROC_CORES> The number of cores to use for parallel processing of verification conditions. [default: 4]

• --vc-timeout <VC_TIMEOUT> A (soft) timeout for the solver, per verification condition, in seconds. [default: 40]

• --check-inconsistency Whether to check consistency of specs by injecting impossible assertions.

• --keep-loops Whether to keep loops as they are and pass them on to the underlying solver.

• --loop-unroll <LOOP_UNROLL> Number of iterations to unroll loops.

• --stable-test-output Whether output for e.g. diagnosis shall be stable/redacted so it can be used in test output.

• --dump Whether to dump intermediate step results to files.