final

README.md

@@ -39,6 +39,13 @@ The Formal Verification (FV) component of the contest is about using the Certora
 - **Support Channels**:
   - For tool-related issues, send a detailed message with a job link in `help-desk` channel in Discord. Remove the anonymousKey component from the link if you wish to limit viewing to Certora employees. 
   - For FV contest questions, use the relevant community verification channel in Discord.
+- **Certora folder**:
+  - Certora folder is made up of 5 folders:
+    - `confs`: configuration files for the tool. There is one per contract. More can be added if needed.
+    - `harnesses`: contracts that inherit base contracts to add extra functionality.
+    - `helpers`: additional contracts/mocks needed for verification.
+    - `mutations`: mutants folder which will be used to evaluate specs.
+    - `specs`: specification used to verify the smart contracts.
 
 ## Incentives
 - 100,000k of the total pool is allocated for FV.

certora/harnesses/modules/BorrowingHarness.sol

@@ -1,9 +1,46 @@
-// SPDX-License-Identifier: GPL-2.0-or-later
 pragma solidity ^0.8.0;
+import "../../../src/EVault/modules/Borrowing.sol";
+import "../../../src/EVault/shared/types/UserStorage.sol";
+import "../../../src/EVault/shared/types/Types.sol";
 import {ERC20} from "../../../lib/ethereum-vault-connector/lib/openzeppelin-contracts/contracts/token/ERC20/ERC20.sol";
 import "../AbstractBaseHarness.sol";
-import "../../../src/EVault/modules/Borrowing.sol";
 
-contract BorrowingHarness is Borrowing, AbstractBaseHarness {
-    constructor(Integrations memory integrations) Borrowing (integrations) {}
+uint256 constant SHARES_MASK = 0x000000000000000000000000000000000000FFFFFFFFFFFFFFFFFFFFFFFFFFFF;
+
+contract BorrowingHarness is AbstractBaseHarness, Borrowing {
+    constructor(Integrations memory integrations) Borrowing(integrations) {}
+
+    function initOperationExternal(uint32 operation, address accountToCheck)
+        public 
+        returns (VaultCache memory vaultCache, address account)
+    {
+        return initOperation(operation, accountToCheck);
+    }
+
+    function getTotalBalance() external view returns (Shares) {
+        return vaultStorage.totalShares;
+    }
+
+    function toAssetsExt(uint256 amount) external pure returns (uint256){
+        return TypesLib.toAssets(amount).toUint();
+    }
+
+    function unpackBalanceExt(PackedUserSlot data) external view returns (Shares) {
+        return Shares.wrap(uint112(PackedUserSlot.unwrap(data) & SHARES_MASK));
+    }
+
+    function getUserInterestAccExt(address account) external view returns (uint256) {
+        return vaultStorage.users[account].interestAccumulator;
+    }
+
+    function getVaultInterestAccExt() external returns (uint256) {
+        VaultCache memory vaultCache = updateVault();
+        return vaultCache.interestAccumulator;
+    }
+
+     function getUnderlyingAssetExt() external returns (IERC20) {
+        VaultCache memory vaultCache = updateVault();
+        return vaultCache.asset;
+    }
+
 }

certora/specs/Base.spec

@@ -36,6 +36,8 @@ methods {
     function _.safeTransferFrom(address token, address from, address to, uint256 value, address permit2) internal with (env e)=> CVLTrySafeTransferFrom(e, from, to, value) expect (bool, bytes memory);
     function _.tryBalanceTrackerHook(address account, uint256 newAccountBalance, bool forfeitRecentReward) internal => NONDET;
     function _.balanceTrackerHook(address account, uint256 newAccountBalance, bool forfeitRecentReward) external => NONDET;
+
+    function _.mulDiv(uint144 a, uint256 b, uint256 c) internal => CVLMulDiv(a, b, c) expect uint144; 
 }
 
 ghost CVLGetQuote(uint256, address, address) returns uint256 {
@@ -54,6 +56,12 @@ function CVLGetQuotes(uint256 amount, address base, address quote) returns (uint
     );
 }
 
+function CVLMulDiv(uint144 a, uint256 b, uint256 c) returns uint144 {
+    mathint result = (a * b) / c; 
+    require result <= max_uint144;
+    return assert_uint144(result); 
+}
+
 ghost address oracleAddress;
 ghost address unitOfAccount;
 function CVLProxyMetadata() returns (address, address, address) {

certora/specs/Borrowing.spec

@@ -3,7 +3,7 @@ import "./Base.spec";
 methods {
     function _.emitTransfer(address, address, uint256) external => NONDET;
     // dispatch and use MockFlashBorrow if more detailed implementation is required
-    function onFlashLoan(address, address, uint256, uint256, bytes) external => NONDET;
+    function _.onFlashLoan(address, address, uint256, uint256, bytes) external => NONDET;
 }
 
 // used to test running time