Movement Logo

Formal Verification in Move: Determining When Functions Abort

Franck Cassez

Move is a verification-friendly programming language enabling users to specify and formally verify smart contracts.

In this post, we identify the conditions under which a function aborts, meaning it fails to complete its intended execution. Understanding these conditions is crucial for ensuring software reliability, especially in critical systems like dApps implemented with smart contracts, where unexpected failures can have significant consequences.

Our objective is to formally and automatically prove that a function aborts only under specific, well-defined circumstances.

Why is Proving This Important?

First, aborting the execution of a smart contract is a fundamental programming pattern, essential for ensuring correctness and security. You want a function to abort under well-defined conditions, including:

  • arithmetic errors: overflow, underflow, division by zero, etc

  • invalid memory accesses: for instance an array out-of-bounds, or

  • invalid asset transfers: for instance when the sender’s balance is insufficient to complete a transaction.

This defensive mechanism acts as a safeguard, protecting the contract from common vulnerabilities and malicious exploitation. By halting (aborting) execution in unsafe scenarios, it prevents unintended behavior and potential financial loss. At the same time, you don’t want your function to abort when it shouldn’t. Spurious aborts, especially during executions that are supposed to be valid, are red flags that point to flaws or bugs in the contract’s logic. Ensuring that a function aborts only under the right circumstances is critical for building reliable and predictable dApps.

Second, there is a subtle interaction between aborts and postconditions. Postconditions (specified by ensures in Move) are properties guaranteed to hold when the function terminates. Postconditions are valid only for execution paths where the function completes successfully without aborting.

In extreme cases, such as the example below, if a function aborts for all inputs, it effectively has no execution paths that terminate.

fun always_aborts() {
    assert!(false);
}

spec always_aborts {
    ensures 1 == 2;
}

In this situation, it becomes possible to prove any postcondition, even logically absurd statements like 1 == 2. This occurs because, without any successful execution paths, there are no counterexamples to invalidate the postcondition, rendering it trivially true.

A less trivial case is a postcondition of the form P ⟹ Q (read "P implies Q"). The logical connector ⋅⟹⋅(implication) specifies that when P holds, we expect Q to hold, too. If the function always aborts when P holds, the postcondition P ⟹ Q is vacuously true and does not provide any useful guarantees.

This underscores the importance of thoroughly understanding and rigorously proving the conditions under which a function aborts. Doing so is critical not only for verifying the correctness of the function but also for preserving the integrity of the formal verification process itself.

In this post, I'll explain how I use the Move Specification Language and the Move Prover to determine the conditions under which a function aborts.

Disclaimer: hereafter I have listed some rules I follow to verify Move code, and these are my own rules, they are not suggested nor endorsed by the Move language and prover maintainers.

We use the Aptos Move framework and the examples in this post are checked with Aptos CLI 5.1.0. In the sequel when we write "the code … verifies," we mean that the result of the command aptos move prove is Success.

Checking Abort Conditions

If you run the Move Prover with the default configuration (aptos move prove), it does not check whether a function aborts.

For instance, the code below with an empty specification (lines 18–20) for inc_count verifies:

/// Capturing abort conditions in a Move module
module 0x02::FindAborts {

  const ENOT_EVEN: u64 = 0x03;
    
  struct Count has key {
    val: u64
  }

  /// Increment the resource by `x` units
  entry fun inc_count(x: u64) acquires Count {
    // the following aborts with error code ENOT_EVEN if x is not even
    assert!(x % 2 == 0, ENOT_EVEN);
    let c = borrow_global_mut<Count>(@0x02);
    c.val = c.val + x;
  }

  spec inc_count {

  }
}

To make sure the prover checks whether a function aborts, you can set the flag (prover directive) aborts_if_is_strict to true.

Rule 1: Set aborts_if_is_strict to true to force the prover to check whether a function aborts.

This can be done within the specification of a function and in that case it applies to this function only, or module-wide and in that case it applies to every function in the module. The latter strategy is applied in this code:

/// Capturing abort conditions in a Move module
module 0x02::FindAborts {

  spec module {
    pragma aborts_if_is_strict = true;
  }

  const ENOT_EVEN: u64 = 0x03;

  struct Count has key {
    val: u64
  }

  /// Increment the resource by `x` units
  entry fun inc_count(x: u64) acquires Count {
    // the following aborts with error code ENOT_EVEN if x is not even
    assert!(x % 2 == 0, ENOT_EVEN);
    let c = borrow_global_mut<Count>(@0x02);
    c.val = c.val + x;
  }

  spec inc_count {

  }
}

Running the Prover on the code snippet above now results in a verification error:

find-aborts git:(master) ✗ aptos move prove
[INFO] preparing module 0x2::FindAborts
[INFO] transforming bytecode
[INFO] generating verification conditions
[INFO] 1 verification conditions
[INFO] running solver
[INFO] 0.221s build, 0.005s trafo, 0.017s gen, 0.608s verify, total 0.851s
error: abort not covered by any of the `aborts_if` clauses
   ┌─ /Users/franck/development/move-learning/find-aborts/sources/find-aborts.move:22:5
   │  
17 │           assert!(x % 2 == 0, ENOT_EVEN);
   │           ------ abort happened here with code 0x3
   ·  
22 │ ╭     spec inc_count {
23 │ │ 
24 │ │     }
   │ ╰─────^
   │  
   =     at /Users/franck/development/move-learning/find-aborts/sources/find-aborts.move:15: inc_count
   =         x = 1
   =     at /Users/franck/development/move-learning/find-aborts/sources/find-aborts.move:17: inc_count
   =         ABORTED

{
  "Error": "Move Prover failed: exiting with verification errors"
}

If you are familiar with Move, you may indeed have identified a few cases (arithmetic errors, non-existence of a resource) where this function aborts. We may want to precisely identify these scenarios.

Here are some possible scenarios that yield to an abort:

  • the parameter x is not an even number (line 17), or

  • the resource Count does not exists (line 18), or

  • an overflow in the addition (line 19).

The prover can automatically detect these scenarios. In the example above, it has detected a possible abort in the code but the specification does not contain a corresponding aborts_if clause. Moreover, there is an example of how the function aborts when it is called with x == 1 (line 20).

At this point there are a few options:

  1. identify the conditions for which the function aborts. This can de done using aborts_if or its variants aborts_if [condition]... with [error code] (see documentation).

  2. or simply identify the possible error codes (e.g., EXECUTION_FAILURE that capture the types of the errors that correspond to aborts.

Specifying abort Conditions with the Move Specification Language

With the aborts_if_is_strict flag set to true, we have to identify all possible cases for which the inc_count function aborts. With the Move Specification Language, the cases are captured by (logical) predicates. A predicate is function that evaluates to either true or false. We can use predicates to define sets of values. For example, the predicate x % 2 == 0 is true only for even values of x. To determine precisely when a function aborts, we can try to identify the values of the inputs and global variables that trigger an abort:

We have to find a predicate P such that the function inc_count aborts if and only if the predicate P is true.

In principle, if there are many scenarios under which the function aborts, we can write a disjunctive predicate which is a logical or of many sub-predicates. But that quickly results in very complicated an unreadable logical formulas. The Move Specification Language allows you to enumerate the cases with a list of aborts_if and treat the list as a logical or (disjunction). The Move Specification Language supports a rich type of logical expressions to specify the predicates:

  • x % 2 != 0: a standard logical formulas with arithmetic expressions;

  • global<Count>(@0x02).val + x > MAX_U64: the largest value that can fit within 64 bits, MAX_U64 can be used to specify overflow conditions;

  • exists<Count>(@0x02): the predicate exists that is true if and only if a resource exists at a given address.

For instance the code below lists three possible predicates (lines 23–26) that result in inc_count to abort:

/// Capturing abort conditions in a Move module
module 0x02::FindAborts {

  spec module {
    pragma aborts_if_is_strict = true;
  }

  const ENOT_EVEN: u64 = 0x03;

  struct Count has key {
    val: u64
  }

  /// Increment the resource by `x` units
  entry fun inc_count(x: u64) acquires Count {
    // the following aborts with error code ENOT_EVEN if x is not even
    assert!(x % 2 == 0, ENOT_EVEN);
    let c = borrow_global_mut<Count>(@0x02);
    c.val = c.val + x;
  }

  spec inc_count {
    aborts_if global<Count>(@0x02).val + x > MAX_U64 with EXECUTION_FAILURE;
    aborts_if !exists<Count>(@0x02) with EXECUTION_FAILURE;
    aborts_if x % 2 != 0 with ENOT_EVEN;
  }
}

This code verifies which implies that inc_count aborts if and only if one of the three conditions is satisfied. We have identified precisely when inc_count aborts, and in this example I have used the variant of aborts_if that also captures the error code associated with the abort.

It may not be easy to capture all of the abort cases in one go, and what I usually do is try to identify them one by one. To do so, I follow

Rule 2: Temporarily set aborts_if_is_partial to true to verify that a function aborts if a condition is satisfied. This enables to discover abort conditions in an incremental manner.

By setting the aborts_if_is_partial to true the prover checks that a function aborts if a condition is satisfied but not only if. The following code verifies:

/// Capturing abort conditions in a Move module
module 0x02::FindAborts {

  spec module {
    pragma aborts_if_is_strict = true;
  }

  const ENOT_EVEN: u64 = 0x03;

  struct Count has key {
    val: u64
  }

  /// Increment the resource by `x` units
  entry fun inc_count(x: u64) acquires Count {
    // the following aborts with error code ENOT_EVEN if x is not even
    assert!(x % 2 == 0, ENOT_EVEN);
    let c = borrow_global_mut<Count>(@0x02);
    c.val = c.val + x;
  }

  spec inc_count {
    pragma aborts_if_is_partial = true;

    aborts_if global<Count>(@0x02).val + x > MAX_U64 ;
    aborts_if !exists<Count>(@0x02) ;
    // aborts_if x % 2 != 0;
  }
}

You can check that setting the aborts_if_is_partial flag to false will result in the prover identifying a missing abort case. When there are many possible abort cases to identify or when we construct the specification, it may be convenient to temporarily set aborts_if_is_partial to true. When we think we have identified all the abort cases, we can set it to false and re-verify (aptos move prove) to make sure we have not missed any cases and the function aborts if and only if one of the conditions in the list of aborts_if is satisfied.

Identifying Error Codes that are the Result of an abort

Identifying the precise conditions for which a function aborts may be non-trivial, and sometimes a more abstract approach may be used: identifying the error codes of the abort cases.

This can be done by using the aborts_with clause (line 23 below) as follows:

/// Capturing abort conditions in a Move module
module 0x02::FindAborts {

  spec module {
    pragma aborts_if_is_strict = true;
  }

  const ENOT_EVEN: u64 = 0x03;

  struct Count has key {
    val: u64
  }

  /// Increment the resource by `x` units
  entry fun inc_count(x: u64) acquires Count {
    // the following aborts with error code ENOT_EVEN if x is not even
    assert!(x % 2 == 0, ENOT_EVEN);
    let c = borrow_global_mut<Count>(@0x02);
    c.val = c.val + x;
  }

  spec inc_count {
    aborts_with EXECUTION_FAILURE, ENOT_EVEN;
  }
}

In this configuration, the prover ensures that the list of error codes specified in the aborts_with clause comprehensively includes all possible error codes that the function could generate in any abort scenario. Specifically, for the inc_count function, this means that whenever the function aborts, the resulting error code is guaranteed to be either EXECUTION_FAILURE or ENOT_EVEN.

Mixed Approach

Identifying all the conditions under which a function aborts is not always straightforward. For example, consider a function foo that performs a check on the input x as illustrated in the code snippet below. The implementation of foo might be complex, involving nested function calls or computations on x before performing the check. As a result, foo could abort after a series of nested calls, making it challenging to pinpoint the exact condition responsible for the abort, especially when it occurs deep within the call stack.

This is why a mixed approach can sometimes be effective:

Rule 3: Identify as many abort conditions as possible. For cases that are missing or difficult to pinpoint, focus on specifying the corresponding error code.

The code below illustrates this approach:

/// Capturing abort conditions in a Move module
module 0x02::FindAborts {

  spec module {
    pragma aborts_if_is_strict = true;
  }

  const E_FOO: u64 = 0x03;

  struct Count has key {
    val: u64
  }

  /// Increment the resource by `x` units
  entry fun inc_count(x: u64) acquires Count {
    // the following aborts with error code ENOT_EVEN if x is not even
    foo(x);
    let c = borrow_global_mut<Count>(@0x02);
    c.val = c.val + x;
  }

  spec inc_count {
    pragma aborts_if_is_partial = true;
    aborts_if global<Count>(@0x02).val + x > MAX_U64 with EXECUTION_FAILURE;
    aborts_if !exists<Count>(@0x02) with EXECUTION_FAILURE;    
    // in the next clause, EXECUTION_FAILURE can be ommitted
    aborts_with EXECUTION_FAILURE, E_FOO;
  }

  // perform a computation on the input and check a property
  fun foo(x: u64) {   
    let y = x / 2;
    assert!(y % 3 == 0, E_FOO);
  }

  spec foo {
    //  Disable check of aborts for foo
    pragma aborts_if_is_strict = false;
  }
}

Specifying exactly when foo aborts when it is called from inc_count can be challenging. To address this, we can identify some of the abort conditions (lines 24–25) and specify the set of possible error codes (line 27).

In this configuration, the prover ensures that:

  • inc_count aborts if either of the conditions specified at lines 24 or 25 is satisfied (a partial list of abort conditions).

  • If inc_count does abort, the error code is guaranteed to be either EXECUTION_FAILURE or E_FOO.

Summary

This is how the Move prover detects abort conditions in specifications:

  • The prover only checks for abort conditions if at least one aborts_if clause is present or if pragma aborts_if_is_strict = true; is set (which is equivalent to specifying aborts_if false;).

  • By default, the prover ensures that aborts_if clauses are exhaustive – meaning all possible abort conditions must be captured. If verification succeeds, it guarantees that the function aborts if and only if one of the specified conditions holds.

  • If you want the prover to check that each aborts_if condition actually results in an abort but do not require exhaustive coverage, you can set aborts_if_is_partial = true. If verification succeeds, it ensures that whenever a specified condition holds, the function aborts.

To specify error codes for aborts, you can use aborts_if Cond with ErrorCode or aborts_with ErrorCode. If at least one aborts_if Cond with ErrorCode or aborts_with ErrorCode clause is present, the prover ensures that all possible error codes are covered, either in an aborts_if ... with ... or aborts_with clause.

Acknowledgments

I'd like to thank Teng Zhang and Wolfgang Grieskamp (Aptos Labs) for their helpful guidance and feedback.