1. How do specs compose?

The Move Prover will use the spec of a function to verify other functions that call it.

For example, if we have a function foo that calls bar, and we have a spec bar_spec for bar, the Move Prover will use bar_spec to verify foo.

Marking a spec with #[spec(prove)] will make the prover attempt to prove it. Leaving out the prove attribute will make the prover use the spec to verify other functions, but not attempt to prove it.

2. How do I focus the prover on a particular spec?

Adding the focus attribute to a spec/scenario (#[spec(prove, focus)) will make the prover only attempt to prove this particular spec. You can apply focus to multiple specs at once, and the prover will attempt to prove all of them in a single run.

<aside> ⚠️

We do not recommend committing this change to the repository, as it will make the prover only attempt to prove a single spec, instead of all specs in the project.

</aside>

3. How do I specify a scenario, instead of writing a spec for a particular function?

Scenarios are specified using the #[spec] attribute on a function that does not end in _spec and does not have a target attribute.

Unlike function specs, scenarios are not required to call the function they are targeting, as there is no such target.

4. How do I write a spec for a function in a different module?

The target attribute can be used to specify which function is being specified, instead of relying on the _spec suffix.

By convention, a function named <function_name>_spec targets <function_name> when placed in the same module.

If we want to specify a function that is not in the same module, we can use the target attribute to specify which function is being specified. For example, if we have a function foo and want to write a spec with a different name, we can use the target attribute to specify that it targets foo:

module 0x42::foo {
    public fun inc(x: u64): u64 {
        x + 1
    }
}

module 0x43::foo_spec {
    // ...

    #[spec(prove, target = foo::inc)]
    public fun this_is_not_inc_spec_yet_it_targets_inc(x: u64): u64 {
        let res = foo::inc(x);
        // ...
        res
    }
}

5. How do I access private members or functions when writing a spec?

Specs are just regular Move code so they cannot access private members or functions. But this can be necessary, especially when writing specs for functions in a different module. To go around this limitation, you can use #[spec_only] do add getters and other accessor functions as needed. As the name says, these accessors are only visible to specs and are not included in the regular compilation.

6. How do I specify the conditions under which a transaction aborts?

A transaction aborts on certain arithmetic conditions (e.g. overflows) as well as on failure of assert! statements -- see Abort and Assert.