From d35df03884b5d4d687c3c537c21b73d11f402e97 Mon Sep 17 00:00:00 2001 From: Jacob Stenum Czepluch Date: Tue, 16 Dec 2025 18:29:39 +0100 Subject: [PATCH] fix 404 github links, remove section for assertion that doesn't exist' --- assertions-book/assertions/aave-v3-suite.mdx | 19 ++++++------------- 1 file changed, 6 insertions(+), 13 deletions(-) diff --git a/assertions-book/assertions/aave-v3-suite.mdx b/assertions-book/assertions/aave-v3-suite.mdx index afb6eca..21f76c9 100644 --- a/assertions-book/assertions/aave-v3-suite.mdx +++ b/assertions-book/assertions/aave-v3-suite.mdx @@ -31,11 +31,9 @@ In order to showcase the real power of assertions, we have introduced a bug in t Anyone borrowing exactly `333e6` tokens will receive double the amount of tokens they would normally receive if they borrowed any other amount. -The bug can be found in the [BorrowLogic.sol](https://github.com/phylaxsystems/aave-v3-origin/tree/main/src/protocol/libraries/logic/BorrowLogic.sol#L128-L144) file. +The bug can be found in the [BorrowLogic.sol](https://github.com/phylaxsystems/aave-v3-origin/blob/main/src/contracts/protocol/libraries/logic/BorrowLogic.sol#L137-L141) file. - -**DO NOT USE THIS VERSION OF AAVE V3 IN PRODUCTION!** - +**DO NOT USE THIS VERSION OF AAVE V3 IN PRODUCTION!** ## Key Features @@ -66,7 +64,7 @@ These demonstrate assertion capabilities but could be implemented in Solidity: ## Assertion Collections -### Production Assertions (High Value) +### Production Assertions #### Core Invariants @@ -97,18 +95,12 @@ These demonstrate assertion capabilities but could be implemented in Solidity: - Balance change verification using event logs - Works with complex call patterns -### Showcase Assertions (Demonstrative) +### Showcase Assertions #### Operation Validation -- **[BorrowingInvariantAssertions](https://github.com/phylaxsystems/aave-v3-origin/tree/main/assertions/src/showcase/BorrowingInvariantAssertions.a.sol)** - Standard borrow checks: - - Liability decrease verification - - Health factor maintenance - - Reserve state consistency - - Borrow cap enforcement - - Balance/debt tracking - - **[LendingInvariantAssertions](https://github.com/phylaxsystems/aave-v3-origin/tree/main/assertions/src/showcase/LendingInvariantAssertions.a.sol)** - Standard supply/withdrawal checks: + - Reserve state validation - Supply cap enforcement - Balance change verification @@ -152,6 +144,7 @@ These demonstrate assertion capabilities but could be implemented in Solidity: ## Intentional Bugs 1. **333e6 Borrow Bug**: Borrowing exactly 333e6 tokens returns double amount + - Location: `BorrowLogic.sol` lines 128-144 - Test: `test_BASE_INVARIANT_A_DebtTokenSupply_333e6Bug()`