Learning Certora Prover (Part 1)

Introduction

Predicates, propositional logic and quantifiers are basic concepts of mathematical logic useful and needed when doing formal verification.

• Propositional Logic : basis of mathematical logic, dealing with boolean variables and operations.

  • A propositions is a function where all inputs have type bool and returns a bool and where only logical operators are allowed in the body of the function

    function P(bool Q,bool R)returnsbool{
        return Q&& R;
    }
    // OR // 
    bool P = Q && R;

• Implication Operator : P implies Q means that if P is true then Q is also true , then the statement is true when either both P and Q are true, or when P is false : P ⇒ Q

  • Math : (Q∨R)⟹(P∧S) and CVL (Q || R) => (P && S)

  • Math : (P⟹(Q∨R))∧(¬P⟹S) and CVL (P => (Q || R)) && (!P => S)

• Predicates : function whose return type is bool (returns true or false)

  • function “is n divisible by 3” is a predicate :

    function f(int n) returns bool {
        return 3 * (n / 3) == n;
    }

• Quantifiers : The statement “there exists a natural number n which is divisible by 3” is an example of a quantifier . This statement is true, since n=3 is indeed divisible by 3 . In general, given a predicate f(x) where x belongs to some set S , we can use a quantifier on f to make a statement in one of two ways.

• Exists :

  • in CVL : require (exists uint n. (n % 3) == 0);

  • in solidity :

      function existsDivisibleByThree() external returns (bool) {
        for (uint256 i = 1; i < type(uint256).max; i++) {
          if (i % 3 == 0) return true;
        }
        return false;
      }
    

• ForAll :

  • in CVL : require (forall uint n. (n % 2 == 0) || ((n + 1) % 2 == 0));

  • in solidity :

      function allAreEven() external returns (bool) {
        for (uint256 i = 1; i < type(uint256).max; i++) {
          if (i % 2 != 0 && (i + 1) %2 != 0) return false;
        }
        return true;
      }
    

QUIZ :

1. When is the expression P⟹Q false?

   1. When ¬P∧¬Q is true (i.e. when both P and Q are false)

   2. When P∧Q is true

   3. When ¬P∧Q is true

   4. None of the above

2. When is the expression P∧Q ⟹P true?

   1. Always (it is true in all cases)

   2. Never (it is false in all cases)

   3. True for some cases and false for others

   4. None of the above

3. When is the expression (P∧(Q∨¬P))∧¬Q true?

   1. Always (it is true in all cases)

   2. Never (it is false in all cases)

   3. True for some cases and false for others

4. If we know that the expression P⟹(P∧¬Q) is true, and that P is true, then we can deduce that:

   1. Q is true

   2. Q is false

   3. Q can be either true or false (we can deduce nothing)Answers

Answers ⇒ 4,1,2,2

Basic Structure of a CVL Rule

let’s take the example from this tutorial to explain how to build your CVL rule :

Four sisters, Sara, Ophelia, Nora, and Dawn, were each born in a different one of
the months September, October, November, and December.

"This is terrible," said Ophelia one day. "None of us have an initial that matches
the initial of her birth month."

"I don't mind at all," replied the girl who was born in September.

"That's easy for you to say," said Nora. "It would at least be cool if the initial
of my birth month was a vowel, but no."

In which month was each girl born?

A rule in CVL has the following structure:

rule ruleName(parameters) {
    // Preconditions (require statements)
    // Logic statements
    // Assertions or satisfiability queries
}

Each rule represents a property you want to verify about your system.

1. Define Constants and Data Types

Start by defining any constants or data types you'll use in your verification:

// Define constants for months
definition September() returns uint8 = 9;
definition October() returns uint8 = 10;
definition November() returns uint8 = 11;
definition December() returns uint8 = 12;

2. Create a Rule with Parameters

Define your rule with appropriate parameters:

rule sistersBirthMonths(
    uint8 Sara,
    uint8 Ophelia,
    uint8 Nora,
    uint8 Dawn
) {
    // Rule body will go here
}

3. Add Preconditions with require Statements

Use require statements to establish the constraints from your problem:

// Each sister was born in one of the four months
require Sara >= September() && Sara <= December();
require Ophelia >= September() && Ophelia <= December();
require Nora >= September() && Nora <= December();
require Dawn >= September() && Dawn <= December();

// None of the sisters have initials matching their birth month
require (
    Sara != September() &&
    Ophelia != October() &&
    Nora != November() &&
    Dawn != December()
);

// Additional clues
require Ophelia != September();  // Ophelia is not born in September
require Nora != September();     // Nora is not born in September
require Nora != October();       // Nora's birth month doesn't start with a vowel

4. Enforce Uniqueness Constraints

Make sure that each sister is born in a different month:

// The sisters were born in different months
require (
    Sara != Ophelia &&
    Sara != Nora &&
    Sara != Dawn &&
    Ophelia != Nora &&
    Ophelia != Dawn &&
    Nora != Dawn
);

5. Add Verification Goals

Depending on what you want to verify, add either:

• For finding a solution: satisfy true;

• For proving a specific solution is correct: assert (conditions);

Finding a solution:

satisfy true;

Proving a specific solution is unique:

assert (
    Sara == October() &&
    Ophelia == November() &&
    Nora == December() &&
    Dawn == September()
);

Running Your Verification

To run your verification, use the Certora Prover with your specification file:

certoraRun Empty.sol --verify Empty:sisters.spec --solc solc --rule ruleName

The Certora Prover will either:

• Find values that satisfy your conditions (for satisfy statements)

• Prove your assertion is correct

• Provide a counterexample if your assertion can be violated

That’s it for it , see you in part 2