[Prover] Comparison with Certora (Solidity)

[weeafoov]

Discord user ID

ainoobai

Describe your question in detail.

For a project I need to compare the capability of Certora (prover for Solidity) and the Aptos Move Prover
In that tool it is possible to define properties as the following:

• if f (some function name) reverts/not reverts then some property holds (i.e. something like a !aborts if)
  It is possible to write something similar in the move specification language?

• It is possible to split spec definition in independent spec block, something like

  spec property1aboutfunctionf {

  }
  spec property2aboutfunctionf {

  }
  Where i want to prove different distinct property of some function f (apparently when i do something like that in the source code the properties seems to "collapse" into one single spec block, am i right?),
  (Why do i want that? i need to prove different independent properties over some smart contracts and having all in one spec block makes reading them difficult)

• It is possible to prove properties parametric with respect to the functions defined in a smart contracts? for example, having something like this:

  struct M {
  balance : u64
  }

  public fun inc(x : M) {
  ... increases balance
  }
  public fun dec(x : M){
  ... decreases balance
  }

I want to prove: the only way to decrease balance is to use dec

Also (on an unrelated note) i had some questions #520 on the move prover, but they where left unanswered
It is this the best place to ask such questions/was the questions too long/unclear? (or do I need to ask them somewhere else like discord or the aptos foundation forum etc?)

What error, if any, are you getting?

No response

What have you tried or looked at? Or how can we reproduce the error?

No response

Which operating system are you using?

Linux (Ubuntu, Fedora, Windows WSL, etc.)

Which SDK or tool are you using? (if any)

Aptos CLI

Describe your environment or tooling in detail

No response

[weeafoov]

Also i forgot to ask:

• it is possible to disable some specific checks (for example, disable overflow checks)?

[0xbrw]

cc @junkil-park who will have more context on the move prover

[Medlab-web3]

1. Defining Properties for Revert/Not Revert Scenarios

In Move, the specification language allows you to define preconditions (requires) and postconditions (ensures) to model such properties. While the direct equivalent of Solidity's !aborts if does not exist, you can express similar logic by specifying:

Preconditions (requires) that ensure a function is called under conditions where it won't abort.
Postconditions (ensures) that verify properties of state changes after execution.
For example:

spec fun example_function_spec {
    requires condition_that_ensures_no_abort;
    ensures property_holds;
}

However, the Move Prover does not yet have a direct construct to check explicitly if a function will always revert under certain conditions. This might require custom logic or assumptions to model.