Skip to content

Commit 4b94ca7

Browse files
authored
fix: Fixes on Certora artifacts
1 parent 417a476 commit 4b94ca7

28 files changed

+71
-109
lines changed

certora/basic/applyHarness.patch

Lines changed: 1 addition & 39 deletions
Original file line numberDiff line numberDiff line change
@@ -27,24 +27,10 @@ diff -ruN ../contracts/instances/ATokenInstance.sol contracts/instances/ATokenIn
2727
+ //);
2828
}
2929
}
30-
diff -ruN ../contracts/instances/RwaATokenInstance.sol contracts/instances/RwaATokenInstance.sol
31-
--- ../contracts/instances/RwaATokenInstance.sol 2025-05-22 10:37:46.407985290 +0300
32-
+++ contracts/instances/RwaATokenInstance.sol 2025-05-22 13:05:47.825640088 +0300
33-
@@ -1,8 +1,8 @@
34-
// SPDX-License-Identifier: BUSL-1.1
35-
pragma solidity ^0.8.0;
36-
37-
-import {RwaAToken} from 'src/contracts/protocol/tokenization/RwaAToken.sol';
38-
-import {IPool, IAaveIncentivesController, IInitializableAToken, Errors, VersionedInitializable} from 'src/contracts/protocol/tokenization/AToken.sol';
39-
+import {RwaAToken} from '../protocol/tokenization/RwaAToken.sol';
40-
+import {IPool, IAaveIncentivesController, IInitializableAToken, Errors, VersionedInitializable} from '../protocol/tokenization/AToken.sol';
41-
42-
contract RwaATokenInstance is RwaAToken {
43-
uint256 public constant ATOKEN_REVISION = 1;
4430
diff -ruN ../contracts/protocol/tokenization/base/ScaledBalanceTokenBase.sol contracts/protocol/tokenization/base/ScaledBalanceTokenBase.sol
4531
--- ../contracts/protocol/tokenization/base/ScaledBalanceTokenBase.sol 2025-05-22 12:57:50.864359258 +0300
4632
+++ contracts/protocol/tokenization/base/ScaledBalanceTokenBase.sol 2025-05-22 10:38:43.910375361 +0300
47-
@@ -34,7 +34,7 @@
33+
@@ -34,9 +34,9 @@
4834
}
4935

5036
/// @inheritdoc IScaledBalanceToken
@@ -53,30 +39,6 @@ diff -ruN ../contracts/protocol/tokenization/base/ScaledBalanceTokenBase.sol con
5339
return super.balanceOf(user);
5440
}
5541

56-
diff -ruN ../contracts/protocol/tokenization/RwaAToken.sol contracts/protocol/tokenization/RwaAToken.sol
57-
--- ../contracts/protocol/tokenization/RwaAToken.sol 2025-05-22 10:37:46.407985290 +0300
58-
+++ contracts/protocol/tokenization/RwaAToken.sol 2025-05-22 13:07:53.696364729 +0300
59-
@@ -1,14 +1,14 @@
60-
// SPDX-License-Identifier: BUSL-1.1
61-
pragma solidity ^0.8.10;
62-
63-
-import {SafeCast} from 'src/contracts/dependencies/openzeppelin/contracts/SafeCast.sol';
64-
-import {IERC20} from 'src/contracts/dependencies/openzeppelin/contracts/IERC20.sol';
65-
-import {IAccessControl} from 'src/contracts/dependencies/openzeppelin/contracts/IAccessControl.sol';
66-
-import {Errors} from 'src/contracts/protocol/libraries/helpers/Errors.sol';
67-
-import {AToken} from 'src/contracts/protocol/tokenization/AToken.sol';
68-
-import {IncentivizedERC20} from 'src/contracts/protocol/tokenization/base/IncentivizedERC20.sol';
69-
-import {IRwaAToken} from 'src/contracts/interfaces/IRwaAToken.sol';
70-
-import {IPool} from 'src/contracts/interfaces/IPool.sol';
71-
+import {SafeCast} from '../../../contracts/dependencies/openzeppelin/contracts/SafeCast.sol';
72-
+import {IERC20} from '../../../contracts/dependencies/openzeppelin/contracts/IERC20.sol';
73-
+import {IAccessControl} from '../../../contracts/dependencies/openzeppelin/contracts/IAccessControl.sol';
74-
+import {Errors} from '../../../contracts/protocol/libraries/helpers/Errors.sol';
75-
+import {AToken} from '../../../contracts/protocol/tokenization/AToken.sol';
76-
+import {IncentivizedERC20} from '../../../contracts/protocol/tokenization/base/IncentivizedERC20.sol';
77-
+import {IRwaAToken} from '../../../contracts/interfaces/IRwaAToken.sol';
78-
+import {IPool} from '../../../contracts/interfaces/IPool.sol';
79-
8042
/**
8143
* @title RwaAToken
8244
diff -ruN ../.gitignore .gitignore

certora/basic/conf/AToken.conf

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,6 @@
1111
"process": "emv",
1212
"solc": "solc8.19",
1313
"verify": "ATokenHarness:certora/basic/specs/AToken.spec",
14-
"build_cache": true,
14+
// "build_cache": true,
1515
"msg": "aToken spec"
1616
}

certora/basic/conf/EModeConfiguration.conf

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,6 @@
99
"precise_bitwise_ops": true,
1010
"rule_sanity": "basic", // from time to time, use "advanced" instead of "basic"
1111
"solc": "solc8.19",
12-
"build_cache": true,
12+
// "build_cache": true,
1313
"verify": "EModeConfigurationHarness:certora/basic/specs/EModeConfiguration.spec"
1414
}

certora/basic/conf/NEW-pool-no-summarizations.conf

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -30,11 +30,11 @@
3030
"solc": "solc8.19",
3131
"verify": "PoolHarness:certora/basic/specs/NEW-pool-no-summarizations.spec",
3232
"rule": [
33-
"liquidityIndexNonDecresingFor_cumulateToLiquidityIndex",
33+
"liquidityIndexNonDecreasingFor_cumulateToLiquidityIndex",
3434
"depositUpdatesUserATokenSuperBalance",
3535
"depositCannotChangeOthersATokenSuperBalance"
3636
],
37-
"build_cache": true,
37+
// "build_cache": true,
3838
"parametric_contracts": ["PoolHarness"],
3939
"msg": "pool-no-summarizations::partial rules",
4040
}

certora/basic/conf/NEW-pool-simple-properties.conf

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@
2525
"prover_args": ["-depth 12"], // If reachability passes and the time is ok, this number is ok, dont touch it.
2626
"solc": "solc8.19",
2727
"verify": "PoolHarness:certora/basic/specs/NEW-pool-simple-properties.spec",
28-
"build_cache": true,
28+
// "build_cache": true,
2929
"parametric_contracts": ["PoolHarness"],
3030
"smt_timeout": "6000",
3131
"msg": "pool-simple-properties::ALL",

certora/basic/conf/ReserveConfiguration.conf

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,6 @@
1111
"precise_bitwise_ops": true,
1212
"rule_sanity": "basic", // from time to time, use "advanced" instead of "basic"
1313
"solc": "solc8.19",
14-
"build_cache": true,
14+
// "build_cache": true,
1515
"verify": "ReserveConfigurationHarness:certora/basic/specs/ReserveConfiguration.spec"
1616
}

certora/basic/conf/RwaAToken.conf

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@
1111
"process": "emv",
1212
"solc": "solc8.19",
1313
"verify": "RwaATokenHarness:certora/basic/specs/RwaAToken.spec",
14-
"build_cache": true,
14+
// "build_cache": true,
1515
"msg": "RwaAToken spec",
1616
"server": "production",
1717
}

certora/basic/conf/UserConfiguration.conf

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,6 @@
1212
//],
1313
"precise_bitwise_ops": true,
1414
"solc": "solc8.19",
15-
"build_cache": true,
15+
// "build_cache": true,
1616
"verify": "UserConfigurationHarness:certora/basic/specs/UserConfiguration.spec"
1717
}

certora/basic/conf/VariableDebtToken.conf

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,6 @@
77
"optimistic_loop": true,
88
"process": "emv",
99
"solc": "solc8.19",
10-
"build_cache": true,
10+
// "build_cache": true,
1111
"verify": "VariableDebtTokenHarness:certora/basic/specs/VariableDebtToken.spec"
1212
}

certora/basic/conf/stableRemoved.conf

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
{
22
"assert_autofinder_success": true,
3-
"build_cache": true,
3+
// "build_cache": true,
44
"cache": "aave_inv",
55
"files": [
66
"certora/basic/harness/PoolInstanceHarness.sol"

0 commit comments

Comments
 (0)