chore: merge dev

defi-wonderland · Jul 31, 2024 · 31b093a · 31b093a
2 parents 1583f49 + a793e9d
commit 31b093a
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 12 deletions.
diff --git a/test/invariants/PROPERTIES.md b/test/invariants/PROPERTIES.md
@@ -1,23 +1,23 @@
 | Properties                                                                                  | Type                | Id  | Halmos | Echidna |
 | ------------------------------------------------------------------------------------------- | ------------------- | --- | ------ | ------- |
 | BFactory should always be able to deploy new pools                                          | Unit                | 1   | [x]    | [x]     |
-| BFactory's BDao should always be modifiable by the current BDao                            | Unit                | 2   | [x]    | [x]     |
+| BFactory's BDao should always be modifiable by the current BDao                             | Unit                | 2   | [x]    | [x]     |
 | BFactory should always be able to transfer the BToken to the BDao, if called by it          | Unit                | 3   | [x]    | [x]     |
 | the amount received can never be less than min amount out                                   | Unit                | 4   | :(     | [x]     |
 | the amount spent can never be greater than max amount in                                    | Unit                | 5   | :(     | [x]     |
-| swap fee can only be 0 (cow pool)                                                           | Valid state         | 6   | [x]    | [x]     |
+| swap fee can only be 0 (cow pool)                                                           | Valid state         | 6   |        | [x]     |
 | total weight can be up to 50e18                                                             | Variable transition | 7   | [x]    | [x]     |
-| BToken increaseApproval should increase the approval of the address by the amount*          | Variable transition | 8   | [x]    | [x]     |
-| BToken decreaseApproval should decrease the approval to max(old-amount, 0)*                 | Variable transition | 9   | [x]    | [x]     |
+| BToken increaseApproval should increase the approval of the address by the amount*          | Variable transition | 8   |        | [x]     |
+| BToken decreaseApproval should decrease the approval to max(old-amount, 0)*                 | Variable transition | 9   |        | [x]     |
 | a pool can either be finalized or not finalized                                             | Valid state         | 10  |        | [x]     |
 | a finalized pool cannot switch back to non-finalized                                        | State transition    | 11  |        | [x]     |
 | a non-finalized pool can only be finalized when the controller calls finalize()             | State transition    | 12  | [x]    | [x]     |
 | an exact amount in should always earn the amount out calculated in bmath                    | High level          | 13  | :(     | [x]     |
 | an exact amount out is earned only if the amount in calculated in bmath is transfered       | High level          | 14  | :(     | [x]     |
 | there can't be any amount out for a 0 amount in                                             | High level          | 15  | :(     | [x]     |
 | the pool btoken can only be minted/burned in the join and exit operations                   | High level          | 16  |        | [x]     |
-| a direct token transfer can never reduce the underlying amount of a given token per BPT     | High level          | 17  | :(     | [x]     |
-| the amount of underlying token when exiting should always be the amount calculated in bmath | High level          | 18  | :(     | [x]     |
+| ~~a direct token transfer can never reduce the underlying amount of a given token per BPT~~ | High level          | 17  | :(     | #     |
+| ~~the amount of underlying token when exiting should always be the amount calculated in bmath~~ | High level          | 18  | :(     | #     |
 | a swap can only happen when the pool is finalized                                           | High level          | 19  |        | [x]     |
 | bounding and unbounding token can only be done on a non-finalized pool, by the controller   | High level          | 20  | [x]    | [x]     |
 | there always should be between MIN_BOUND_TOKENS and MAX_BOUND_TOKENS bound in a pool        | High level          | 21  |        | [x]     |
@@ -30,10 +30,11 @@
 
 > (**) [Trail of Bits ERC20 properties](https://github.com/crytic/properties?tab=readme-ov-file#erc20-tests)
 
-[ ] planed to implement and still to do
-<br>[x] implemented and tested 
-<br>:( implemented but test not passing due to an external factor (tool limitation - eg halmos max unrolling loop, etc) 
-<br>empty not implemented and will not be (design, etc)
+<br>`[ ]` planed to implement and still to do
+<br>`[x]` implemented and tested
+<br>`:(` implemented but test not passing due to an external factor (tool limitation - eg halmos max unrolling loop, etc)
+<br>`#` implemented but deprecated feature / property
+<br>`` empty not implemented and will not be (design, etc)
 
 # Unit-test properties for the math libs (BNum and BMath):
 
@@ -88,3 +89,5 @@ power of a power should mult the exp (x^a)^b == x^(a*b)
 
 calcOutGivenIn should be inv with calcInGivenOut
 calcInGivenOut should be inv with calcOutGivenIn
+~~calcPoolOutGivenSingleIn should be inv with calcSingleInGivenPoolOut~~
+~~calcSingleOutGivenPoolIn should be inv with calcPoolInGivenSingleOut~~
diff --git a/test/invariants/symbolic/Protocol.t.sol b/test/invariants/symbolic/Protocol.t.sol
@@ -23,7 +23,6 @@ contract HalmosBalancer is HalmosTest {
   BCoWPool pool;
 
   address currentCaller = svm.createAddress('currentCaller');
-  // address currentCaller = address(234);
 
   constructor() {
     solutionSettler = address(new MockSettler());
@@ -107,10 +106,10 @@ contract HalmosBalancer is HalmosTest {
       assert(_currentBDao != currentCaller);
     }
   }
+
   /// @custom:property-id 7
   /// @custom:property total weight can be up to 50e18
   /// @dev Only 2 tokens are used, to avoid hitting the limit in loop unrolling
-
   function check_totalWeightMax(uint256[2] calldata _weights) public {
     // Precondition
     BCoWPool _pool = BCoWPool(address(factory.newBPool()));