Revive the Move prover

[cos]

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: kunalabs-io/sui-smart-contracts#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:

[vercel]

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	Dec 18, 2024 3:14pm

3 Skipped Deployments

Name	Status	Preview	Comments	Updated (UTC)
multisig-toolkit	⬜️ Ignored (Inspect)	Visit Preview		Dec 18, 2024 3:14pm
sui-kiosk	⬜️ Ignored (Inspect)	Visit Preview		Dec 18, 2024 3:14pm
sui-typescript-docs	⬜️ Ignored (Inspect)	Visit Preview		Dec 18, 2024 3:14pm