The Last Markdown Editor, Ever

Preliminary Repository's https://cantina.xyz/code/8b94fd62-eea5-46fb-bed6-36ec5adf36af/README.mdhttps://github.com/cantina-forks/thala-modules/tree/mai

Summary

Formal verification of key modules within the Aave V3 codebase was conducted using an aggressive threat modeling approach with the prover. The process rigorously tested abort conditions, state consistency, authorization checks, and asset conservation to ensure secure and correct operation under all scenarios. This verification focused on mitigating potential threats and maintaining protocol integrity, ensuring the reliability of staking and reward mechanisms.

Modules include:

• aave-math
  • math_utilis.move
  • wad_ray_math.move

Spec Overview for aave_math::wad_ray_math.move

  // Specification for wad_to_ray
    spec wad_to_ray {
        // Preconditions
        requires a >= 0; // Ensure non-negative input
        requires a <= U256_MAX / WAD_RAY_RATIO; // Ensure no overflow

        // Postconditions
        ensures result == a * WAD_RAY_RATIO;
        ensures result >= 0; // Result should be non-negative
    }

    // Attach the specification directly to the function
    spec wad_mul {
        // Preconditions
        requires a <= (U256_MAX - HALF_WAD) / b; // Ensure no overflow
        requires a >= 0; // Ensure non-negative input
        requires b >= 0; // Ensure non-negative input

        // Postconditions
        ensures result == if (a == 0 || b == 0) { 0 } else { (a * b + HALF_WAD) / WAD };
        ensures result >= 0; // Result should be non-negative
    }

      // Specification for wad_div
    spec wad_div {
        // Preconditions
        requires b > 0; // Denominator must be non-zero
        requires a <= (U256_MAX - b / 2) / WAD; // Ensure no overflow
        requires a >= 0; // Ensure non-negative input
        requires b >= 0; // Ensure non-negative input

        // Postconditions
        ensures result == if (a == 0) { 0 } else { (a * WAD + b / 2) / b };
        ensures result >= 0; // Result should be non-negative
    }

        // Specification for ray_div
    spec ray_div {
        // Preconditions
        requires b > 0; // Denominator must be non-zero
        requires a <= (U256_MAX - b / 2) / RAY; // Ensure no overflow
        requires a >= 0; // Ensure non-negative input
        requires b >= 0; // Ensure non-negative input

        // Postconditions
        ensures result == if (a == 0) { 0 } else { (a * RAY + b / 2) / b };
        ensures result >= 0; // Result should be non-negative
    }

        // Specification for ray_mul
    spec ray_mul {
        // Preconditions
        //this does not hold true here 
       // requires a <= (U256_MAX - HALF_RAY) / b; // Ensure no overflow
        requires a >= 0; // Ensure non-negative input
        requires b >= 0; // Ensure non-negative input

        // Postconditions
        ensures result == if (a == 0 || b == 0) { 0 } else { (a * b + HALF_RAY) / RAY };
        ensures result >= 0; // Result should be non-negative
    }

    // Specification for ray_to_wad
    spec ray_to_wad {
        // Preconditions
        requires a >= 0; // Ensure non-negative input

        // Postconditions
        ensures result == if (a % WAD_RAY_RATIO >= WAD_RAY_RATIO / 2) { a / WAD_RAY_RATIO + 1 } else { a / WAD_RAY_RATIO };
        ensures result >= 0; // Result should be non-negative
    }

}

Spec Overview for aave_math::math_utilis.move