Difference between definition and function

CVL Support
1

I couldn’t find what’s the difference between a definition and a function since we can do the same thing with a function also, I guess. So what’s the advantage/disadvantage of definitions over functions?

2

A definition and a function are basically the same - they are both macros. There is a slight difference - a definition defines a macro for an expression, while a function encloses a block of code (i.e. multiple lines).
We often use definitions as macros for states, e.g.

definition userNotExist(address user) returns bool = funds[user] == 0 && numberOfTransactions(user) == 0

We use functions to export blocks of codes that are needed in multiple rules, if for many functions we need to make special assumptions for specific invocation of functions from the contract we can do something like that:

 function assumptions_per_function(method f, arg1, arg3, ...){
   arg2; arg4; arg5;
   if (f.selector == functionA(arg1, arg2, ...).selector) {
        require(exp1);
        require(exp2);
        functionA(arg1, arg2);
    } else if (f.selector == functionB(arg3, arg4, arg5, ...).selector) {
        require(exp3);
        functionB(arg1, arg2, arg3, ...);
    } else  {
        calldataarg args;
        f(e, args);
    }
}

Both of them will inline the body into your rule and in essence aren’t that different. Functions probably can do anything definitions can, just a matter of convenience:

  function userNotExist(address user) returns bool{
     bool isExist = funds[user] == 0 && numberOfTransactions(user) == 0;
     return isExist;
  }
1 Like