Ikhlas - AsTETH - AAVE - Certora

.gitignore

@@ -14,4 +14,7 @@ deployed-contracts.json
 coverage
 .coverage_artifacts
 .coverage_cache
-.coverage_contracts
+.coverage_contracts
+.certora_config
+.last_confs
+.certora*

certora/harness/AStETHHarness.sol

@@ -21,5 +21,60 @@ contract AStETHHarness is AStETH {
       return true;
   }
 
+
+/*****************************
+ *    IKHLAS - i01001        *
+ *****************************/
+
+  function _getRevision() public returns (uint256){
+    return getRevision();
+  }
+
+  function getChainID() external view returns (uint256) {
+    uint256 id;
+    assembly {
+        id := chainid()
+    }
+    return id;
+}
+
+  function _getDecimals() public returns (uint256){
+    return decimals();
+  }
+
+  function _gettoInternalAmount(    uint256 _amount,
+    uint256 _stEthRebasingIndex,
+    uint256 _aaveLiquidityIndex) public returns (uint256){
+    return _toInternalAmount(_amount, _stEthRebasingIndex, _aaveLiquidityIndex);
+  }
+
+
+    function _getscaledTotalSupply(    uint256 _rebasingIndex) public returns (uint256){
+    return _scaledTotalSupply(_rebasingIndex);
+  }
+
+    function _getNonces(address _address) public returns (uint256){
+    return _nonces[ _address];
+  }
+
+
+    function _gettransfer(address from, address to, uint256 amount, bool validate) public {
+    _transfer( from, to, amount, validate);
+  }
+
+
+    function _gettransfer2(address from, address to, uint256 amount) public {
+    _transfer( from, to, amount);
+  }
+
+
+   function _getscaledBalanceOf(address user, uint256 rebasingIndex) public returns (uint256){
+    return _scaledBalanceOf(user, rebasingIndex);
+  }
+
+   function _getstEthRebasingIndex() public returns (uint256){
+    return _stEthRebasingIndex();
+  }
+
 
 }

certora/harness/DummyERC20A.sol

@@ -7,4 +7,5 @@ contract DummyERC20A is DummyERC20Impl {
     function getPooledEthByShares(uint256 _sharesAmount) external view returns (uint256) {
         return 1000000000000000000000000000; // = one RAY
     }
-}
+}
+