Certora AcceleratingDistributor verification

.gitignore

@@ -14,6 +14,6 @@ artifacts
 .certora*
 resource_errors.json
 last_conf*
-
+.vscode
 certora*.txt
 .zip-output-url.txt

certora/AcceleratingDistributor/Makefile

@@ -12,10 +12,9 @@ help:
 	@echo "  make $(MUNGED_DIR): create $(MUNGED_DIR) directory by applying the patch file to $(CONTRACTS_DIR)"
 	@echo "  make record: record a new patch file capturing the differences between $(CONTRACTS_DIR) and $(MUNGED_DIR)"
 
-munged:  $(wildcard $(CONTRACTS_DIR)/*.sol) $(PATCH)
-	rm -rf $@
-	cp -r $(CONTRACTS_DIR) $@
-	patch -p0 -d $@ < $(PATCH)
+munge:
+	cp $(AcceleratingDistributor_Origin) $(MUNGED_DIR)
+	patch -d $(MUNGED_DIR) < $(PATCH)
 
 record:
 	diff -ruN $(AcceleratingDistributor_Origin) $(AcceleratingDistributor_munged) | sed 's+\$(AcceleratingDistributor_Origin)/++g' | sed 's+$(AcceleratingDistributor_munged)++g' > $(PATCH)

certora/AcceleratingDistributor/README.md

@@ -33,9 +33,14 @@ simply add a ':' after the name of the file and then the name of the contract. e
 ## Running Instructions
 To run a verification job:
 
-1. Open terminal and `cd` your way to the UMA/packages/core directory.
+1. Open terminal and `cd` your way to the across-token directory.
 
-2. Run the script you'd like to get results for:
-    ```
-    sh certora/AcceleratingDistributor/scripts/verifyAsserter.sh
-    ```
+2. For first time verification, after pulling from git, go to ./certora/AcceleratingDistributor/
+and then run 'make munge'. This will apply the changes recorded in applyHarness.patch to the munged folder, where the contracts are stored.
+
+3. Go back to core directory ../ 
+
+4. Run the script you'd like to get results for:
+   ```
+   sh certora/AcceleratingDistributor/scripts/verifyAD.sh
+   ```

certora/AcceleratingDistributor/applyHarness.patch

@@ -1,38 +1,31 @@
---- ../../contracts/AcceleratingDistributor.sol	2022-12-21 11:05:45.930780900 +0200
-+++ 	2023-01-03 10:32:05.107472900 +0200
-@@ -15,8 +15,8 @@
-  * only compatible with standard ERC20 tokens, and not tokens that charge fees on transfers, dynamically change
-  * balance, or have double entry-points. It's up to the contract owner to ensure they only add supported tokens.
+--- ../../contracts/AcceleratingDistributor.sol	2023-01-23 18:58:13.479444800 +0200
++++ 	2023-01-23 19:03:39.828585100 +0200
+@@ -18,8 +18,8 @@
+  * they only add supported tokens, and that staking token configurations are applied correctly.
+  * @dev This contract is inspired by the Synthetix staking contract, and the Ampleforth geyser.
   */
 -
 -contract AcceleratingDistributor is ReentrancyGuard, Ownable, Multicall {
 +// Certora: remove MultiCaller inheritance due to technical issues.
 +contract AcceleratingDistributor is ReentrancyGuard, Ownable {
      using SafeERC20 for IERC20;
 
-     IERC20 public immutable rewardToken;
-@@ -296,12 +296,12 @@
-      * was originally audited and deployed with this function being public. Its useful for testing if this function is
-      * public but it can return nonsensical values if the stakedToken precision is fewer than 18 decimals.
-      * @dev the value returned is represented by a uint256 with fixed precision of (18 + 18 - X) decimals, where
--     * X = decimals of the stakedToken. This is becauseof how the return value is divided by `cumulativeStaked`
--     * which has the same precisionas stakedToken.
-+     * X = decimals of the stakedToken. This is because of how the return value is divided by `cumulativeStaked`
-+     * which has the same precision as stakedToken.
+     /**************************************
+@@ -336,7 +336,7 @@
       * @param stakedToken The address of the staked token to query.
       * @return uint256 Total base reward per token that will be applied, pro-rata, to stakers.
       */
 -    function baseRewardPerToken(address stakedToken) public view returns (uint256) {
-+    function baseRewardPerToken(address stakedToken) public virtual view returns (uint256) {
++    function baseRewardPerToken(address stakedToken) public view virtual returns (uint256) {
          StakingToken storage stakingToken = stakingTokens[stakedToken];
          if (stakingToken.cumulativeStaked == 0) return stakingToken.rewardPerTokenStored;
 
-@@ -320,7 +320,7 @@
+@@ -355,7 +355,7 @@
       * @param account The address of the user to query.
       * @return uint256 User multiplier, applied to the baseRewardPerToken, when claiming rewards.
       */
 -    function getUserRewardMultiplier(address stakedToken, address account) public view returns (uint256) {
-+    function getUserRewardMultiplier(address stakedToken, address account) public virtual view returns (uint256) {
++    function getUserRewardMultiplier(address stakedToken, address account) public view virtual returns (uint256) {
          UserDeposit storage userDeposit = stakingTokens[stakedToken].stakingBalances[account];
          if (userDeposit.averageDepositTime == 0 || userDeposit.cumulativeBalance == 0) return 1e18;
          uint256 fractionOfMaxMultiplier = ((getTimeSinceAverageDeposit(stakedToken, account)) * 1e18) /

certora/AcceleratingDistributor/munged/.gitignore

@@ -0,0 +1,2 @@
+*
+!.gitignore