Description

This PR adds back the Sui Move prover with significant changes and enhancements.

The most important change is that the prover no longer uses special syntax. The specifications are now given via special functions, macros, naming conventions and annotations. This has several advantages, including:

making changes to the Move language does not require making sure the changes are compatible with the prover; for example, the old prover did not support tuples as it would have required special wiring
the syntax is much more flexible; for example, a variable used by multiple requires can be extracted out
developers do not need to learn new language features, it is more akin to learning a new sdk or library

The prover now supports:

arithmetic precision and rounding direction
overflow/underflow conditions
loop invariants
struct/type-level invariants
complex vulnerability scenarios

AMM example: https://github.com/kunalabs-io/sui-smart-contracts/pull/9

Features/Changes

std::integer and std::real
- std::integer module for arbitrary-precision integer arithmetic
- std::real module for real number operations
- they are only available for specs
Modeling of native and library functions
prover module
- requires - specifies preconditions (renamed from assume for clarity)
- ensures - specifies postconditions
- asserts - Replaces abort-if with its complement, which is more in line with existing assert statements (can simply copy-paste in many cases)
- invariant! macro for loop invariants
- old! macro for referencing pre-state values
Ghost variables
- declare_global/declare_global_mut prover native commands
- global prover native for state manipulation
- strict checking of ghost variable declarations in specifications.
opaque specifications for functions
- For verification, the implementation of the function is replaced with its specification
- Format: f_spec for function f
- the wiring of requires / ensures /asserts is particularly interesting
- done via structured pre/post-conditions
- The specifications needs to, by convention, follow the following strict format:
  - Identical type signatures
  - contact a single function call to the original function with the same arguments
  - no parameter modification
  - failure-free specification execution ???
- Enforcing the format at compile time or via linting is left for the future
Loop invariants
- placed before loops via invariant! macro
- automatically move to loop headers
- implementation handles mutable and ghost variable havoc
Struct Invariants
- defined via S_inv for struct S
- automatically checked as part of pre-post conditions
- the current implementation is not recursive
Improved Boogie generation
- including skipping unused functions
Eliminating spec code at compile time
- #spec_only annotation
- _spec variables
- automatically eliminating call to verification/spec functions

Test plan

Unit tests covering the new features -- this could be improved
Verification of kai-leverage and DoubleUp codebases

Release notes

The changes should not affect any of the existing functionality. We still recommend extensive testing as we made some changes to the compiler to support spec_only and related.

[ ] Protocol:
[ ] Nodes (Validators and Full nodes):
[ ] Indexer:
[ ] JSON-RPC:
[ ] GraphQL:
[ ] CLI:
[ ] Rust SDK:
[ ] REST API:

The latest updates on your projects. Learn more about Vercel for Git ↗︎

Name	Status	Preview	Comments	Updated (UTC)
sui-docs	✅ Ready (Inspect)	Visit Preview	💬 Add feedback	Nov 21, 2024 5:04pm

3 Skipped Deployments

MystenLabs / sui

Revive the Move prover #20339

Description

Features/Changes

Test plan

Release notes