-
Notifications
You must be signed in to change notification settings - Fork 102
feat: invariant tests #1230
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Open
DhairyaSethi
wants to merge
112
commits into
main
Choose a base branch
from
test/inv
base: main
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
Open
feat: invariant tests #1230
Changes from 67 commits
Commits
Show all changes
112 commits
Select commit
Hold shift + click to select a range
983e275
chore: add full invariant suite (handlers, hooks, specs, replays, REA…
vnmrtz 25693d4
chore: failing replays, adnvanced setup, ci workflow, coverage
vnmrtz 43b4ddd
Merge branch 'main' into enigma-dark-invariant-suite
vnmrtz 576020e
chore: test ci gh app setup
vnmrtz ca48003
chore: change corpus repo
vnmrtz f89d40d
chore: change corpus repo
vnmrtz 3e95511
fix: set x-access-token
vnmrtz ac2583d
fix: typo on compile path
vnmrtz a8b91ce
fix: crytic args
vnmrtz b73826d
chore: move crytic-args to config file
vnmrtz 4f063ff
chore: add --ignore-compile flag
vnmrtz 4b69f73
chore: optimize ci workflowe
vnmrtz f6f6956
chore: optimize workflow
vnmrtz d840de9
chore: change workflow name
vnmrtz 346931d
chore: integrate configurators, filter replays
vnmrtz 35388da
fix: change ci corpus reference
vnmrtz 8a48e88
fix: change ci corpus reference
vnmrtz 768112f
fix: switch runner to aave-latest
vnmrtz 7fcec49
chore: refactor
vnmrtz f400956
chore: hub suite
vnmrtz fbde0fe
chore: fix wrong reserveid invariants wrapper
vnmrtz 8f1a43b
Merge v0.5.6 into enigma-dark-invariant-suite
vnmrtz 05a0e1e
rebase
vnmrtz dce578e
chore: coverage restore, refreshpremium, reportdeficit
vnmrtz 1e3aadf
chore: swep and reclaim coverage
vnmrtz 96572e9
chore: add 4626, roundtrip and availability properties
vnmrtz ac737c6
chore: add hub suite rountrip replays
vnmrtz eaa7ce7
chore: debug replays_6 and fix hub handler assertions
vnmrtz b14a08e
chore: fix invariant assertions
vnmrtz caec11b
chore: cleanup debug artifacts
vnmrtz ded9a96
chore: invariants tightening
vnmrtz f110334
chore: debug replays
vnmrtz 2cc3e90
chore: clean up replays
vnmrtz 66ec557
chore: improve test_replay_7_repay description
vnmrtz b051328
Merge remote-tracking branch 'aave/main' into enigma-dark-invariant-s…
DhairyaSethi d0012be
chore: lint
DhairyaSethi d8ab561
Merge remote-tracking branch 'aave/main' into enigma-dark-invariant-s…
DhairyaSethi a26d6a7
chore: checkpoint
DhairyaSethi 1a02aa7
chore: debug
DhairyaSethi f909853
feat: foundry-invariants working
DhairyaSethi 00e460f
chore: lint
DhairyaSethi 5e612c7
chore: move invariants to separate dir, hopefully tmp
DhairyaSethi 701b7bb
fix: cleanup, new inv, medusa fixes
DhairyaSethi 047c518
chore: ci cleanup
DhairyaSethi 1f36d03
chore: ci cleanup
DhairyaSethi defc15c
chore: ci cleanup
DhairyaSethi f881f98
chore: revert deploy utils, target ci
DhairyaSethi 8d35446
chore: run specified file
DhairyaSethi 1460bbb
chore: force precompile so it picks up correct profile
DhairyaSethi 33c5dc7
Merge remote-tracking branch 'aave/main' into test/inv
DhairyaSethi 358cf00
chore: adapt to latest
DhairyaSethi 5ab024e
chore: rm unnecessary
DhairyaSethi c623ef3
chore: rm create2
DhairyaSethi e9f047c
chore: typo
DhairyaSethi 3759bf0
chore: fix failing hub invariants
DhairyaSethi 5acd24e
chore: grant spoke3 deficit eliminator role
DhairyaSethi 2d560be
fix: more inv
DhairyaSethi 9e2ae79
fix: sum of all invariants by accounting for burnt interest
DhairyaSethi bf392bc
chore: fix premium cond
DhairyaSethi ef40cc7
feat: broader refresh premium target
DhairyaSethi f2a8d4d
temp: clamp ci normal tests
DhairyaSethi 2e8c353
feat: fuzz parser utility
DhairyaSethi 7ccbdb4
feat: run for longer
DhairyaSethi e6a663f
fix: update workflow name to Echidna-Invariants-Hub
DhairyaSethi 2a3f7bc
feat: hub cleanup
DhairyaSethi e4e835b
feat: begin protocol suite cleanup
DhairyaSethi 2d7ac81
chore: fix compile
DhairyaSethi 07fdc96
feat: cleanup + new users invariant
DhairyaSethi 5586fba
chore: update docs
DhairyaSethi 8720895
feat: fix 4626 rt handlers
DhairyaSethi dc112ba
fix: liq fee handler
DhairyaSethi ec164d6
chore: fix minting
DhairyaSethi 17d3dc9
fix: unnecessary cached target asset id
DhairyaSethi 644ed1a
chore: reword low level ret vars
DhairyaSethi 7a2c1bb
chore: minor cleanup
DhairyaSethi 385a675
feat: safe mint for spoke
DhairyaSethi 2fea6f3
chore: group invariants
DhairyaSethi b620f5a
chore: suppress compiler warning
DhairyaSethi 83769cc
chore: naming consistency
DhairyaSethi 18cc79f
chore: fill interfaces
DhairyaSethi cdd364d
chore: fix configurator roles
DhairyaSethi 6427e1c
fix: add new solvency invariants
DhairyaSethi 9d83eea
chore: fix compile
DhairyaSethi 5b33ae4
feat: set user posm to handler
DhairyaSethi 03c8bfc
chore: abstract duplicated helpers
DhairyaSethi 15f1c05
fix: use premiumRay
DhairyaSethi c3e8026
chore: cleanup
DhairyaSethi 5a26b20
feat: expand spoke configurator
DhairyaSethi 9a92a86
fix: include deficit in drawCap
DhairyaSethi 5400b4c
feat: bound and improve fuzzer capacity on hub configurator handler a…
DhairyaSethi ecfaaa5
chore: fix compile
DhairyaSethi fe5f6bb
chore: cleanup
DhairyaSethi 7406934
ci: run echidna in exploration mode as well
DhairyaSethi f8325f2
ci: add medusa
DhairyaSethi 4ac3dba
ci: install slither
DhairyaSethi 4b2fb0d
fix: failing post hook
DhairyaSethi 98a3122
ci: inc medusa runs
DhairyaSethi 8970059
ci: run on 5h timeout
DhairyaSethi add9c16
chore: cleanup
DhairyaSethi a8f06ce
ci: fix echidna run
DhairyaSethi f2bfede
chore: license cleanup
DhairyaSethi 5daa74d
fix: mint fee shares handler
DhairyaSethi 30ce5d5
fix: treasury spoke handler
DhairyaSethi 83023af
feat: hub admin handler
DhairyaSethi 2349920
Merge remote-tracking branch 'aave/main' into test/inv
DhairyaSethi 5135794
chore: adapt to latest
DhairyaSethi ff8da5e
chore: upload artifacts
DhairyaSethi 6e95358
fix: setUserPositionManager handler
DhairyaSethi 6e3b200
tmp: run ci for 1 hour
DhairyaSethi 849af57
chore: whitespace
DhairyaSethi 5fa65fe
feat: run invariants with foundry
DhairyaSethi f80ad64
chore: reduce foundry runs to be under 6h run
DhairyaSethi File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Some comments aren't visible on the classic Files Changed page.
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,45 @@ | ||
| name: Echidna-Invariants | ||
|
|
||
| on: | ||
| push: | ||
| branches: | ||
| - main | ||
| pull_request: | ||
|
|
||
| env: | ||
| FOUNDRY_PROFILE: invariant | ||
|
|
||
| concurrency: | ||
| group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }} | ||
| cancel-in-progress: true | ||
|
|
||
| jobs: | ||
| echidna: | ||
| name: Echidna-Invariants (${{ matrix.mode }}) | ||
| runs-on: ubuntu-latest | ||
|
|
||
| strategy: | ||
| matrix: | ||
| mode: [property, assertion] | ||
|
|
||
| steps: | ||
| - name: Checkout repository | ||
| uses: actions/checkout@v4 | ||
| with: | ||
| submodules: recursive | ||
|
|
||
| - name: Run Foundry setup | ||
| uses: bgd-labs/github-workflows/.github/actions/foundry-setup@main | ||
| with: | ||
| FOUNDRY_VERSION: nightly | ||
|
|
||
| - name: Run Forge Build | ||
| run: forge build --build-info | ||
|
|
||
| - name: Run Echidna ${{ matrix.mode == 'property' && 'Property' || 'Assertion' }} Mode | ||
| uses: crytic/echidna-action@v2 | ||
| with: | ||
| files: invariants/protocol-suite/Tester.t.sol | ||
| contract: Tester | ||
| config: invariants/protocol-suite/_config/echidna_config_ci.yaml | ||
| test-mode: ${{ matrix.mode == 'assertion' && 'assertion' || '' }} |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,45 @@ | ||
| name: Echidna-Invariants-Hub | ||
|
|
||
| on: | ||
| push: | ||
| branches: | ||
| - main | ||
| pull_request: | ||
|
|
||
| env: | ||
| FOUNDRY_PROFILE: invariant | ||
|
|
||
| concurrency: | ||
| group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }} | ||
| cancel-in-progress: true | ||
|
|
||
| jobs: | ||
| echidna: | ||
| name: Echidna-Invariants (${{ matrix.mode }}) | ||
| runs-on: ubuntu-latest | ||
|
|
||
| strategy: | ||
| matrix: | ||
| mode: [property, assertion] | ||
|
|
||
| steps: | ||
| - name: Checkout repository | ||
| uses: actions/checkout@v4 | ||
| with: | ||
| submodules: recursive | ||
|
|
||
| - name: Run Foundry setup | ||
| uses: bgd-labs/github-workflows/.github/actions/foundry-setup@main | ||
| with: | ||
| FOUNDRY_VERSION: nightly | ||
|
|
||
| - name: Run Forge Build | ||
| run: forge build --build-info | ||
|
|
||
| - name: Run Echidna ${{ matrix.mode == 'property' && 'Property' || 'Assertion' }} Mode | ||
| uses: crytic/echidna-action@v2 | ||
| with: | ||
| files: invariants/hub-suite/Tester.t.sol | ||
| contract: Tester | ||
| config: invariants/hub-suite/_config/echidna_config_ci.yaml | ||
| test-mode: ${{ matrix.mode == 'assertion' && 'assertion' || '' }} | ||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,136 @@ | ||
| #!/usr/bin/env python3 | ||
| import re | ||
|
|
||
| def parse_echidna_trace(trace): | ||
| """Parse Echidna trace and extract function calls, parameters, delays, and 'from' addresses.""" | ||
| calls = [] | ||
| last_address = None # Track the last 'from' address | ||
|
|
||
| for line in trace.strip().splitlines(): | ||
| # Parse function calls, including those with underscores | ||
| func_call = re.match(r"Tester\.([a-zA-Z0-9_]+)\(([^)]*)\)", line) | ||
| if func_call: | ||
| func_name = func_call.group(1) | ||
| params = func_call.group(2) | ||
|
|
||
| # Check for 'from' address | ||
| from_address = re.search(r"from: (0x[a-fA-F0-9]+)", line) | ||
| time_delay = re.search(r"Time delay: (\d+)", line) | ||
|
|
||
| # If we have a 'from' address, we need to set it up | ||
| if from_address: | ||
| address = from_address.group(1) | ||
| if address != last_address: | ||
| # Only set up the actor if the address has changed | ||
| calls.append(f"_setUpActor({address});") | ||
| last_address = address | ||
|
|
||
| # Add the delay if it exists | ||
| if time_delay: | ||
| delay_time = time_delay.group(1) | ||
| calls.append(f"_delay({delay_time});") | ||
|
|
||
| # Add the function call | ||
| calls.append(f"Tester.{func_name}({params});") | ||
|
|
||
| # Handle special case of "*wait*" for a delay | ||
| elif "*wait*" in line: | ||
| time_delay = re.search(r"Time delay: (\d+)", line) | ||
| if time_delay: | ||
| delay_time = time_delay.group(1) | ||
| calls.append(f"_delay({delay_time});") | ||
|
|
||
| return calls | ||
|
|
||
| def parse_medusa_trace(trace): | ||
| """Parse Medusa trace and extract function calls, parameters, block, time, and sender information.""" | ||
| calls = [] | ||
| last_address = None # Track the last 'from' address | ||
| last_block = 0 | ||
| last_time = 0 | ||
|
|
||
| for line in trace.strip().splitlines(): | ||
| # Skip empty lines | ||
| if not line.strip(): | ||
| continue | ||
|
|
||
| # Parse Medusa format: number) Contract.function(types)(values) (metadata) | ||
| medusa_pattern = r"(?:\d+\))?\s*Tester\.([a-zA-Z0-9_]+)\([^)]*\)\(([^)]*)\)\s*\(block=(\d+),\s*time=(\d+).*sender=(0x[a-fA-F0-9]+)\)" | ||
| match = re.search(medusa_pattern, line) | ||
|
|
||
| if match: | ||
| func_name = match.group(1) | ||
| params = match.group(2) | ||
| block = int(match.group(3)) | ||
| time = int(match.group(4)) | ||
| address = match.group(5) | ||
|
|
||
| if (address == "0x10000"): | ||
| actor = "USER1" | ||
| elif (address == "0x20000"): | ||
| actor = "USER2" | ||
| elif (address == "0x30000"): | ||
| actor = "USER3" | ||
|
|
||
| # If sender address changed, set up the new actor | ||
| if address != last_address: | ||
| calls.append(f"_setUpActor({actor});") | ||
| last_address = address | ||
|
|
||
| # Add block/time delay if needed | ||
| if time > last_time: | ||
| # Medusa reports absolute timestamps, so we calculate the difference | ||
| # between consecutive transactions to determine the delay | ||
| time_diff = time - last_time | ||
| if time_diff > 0: | ||
| calls.append(f"_delay({time_diff});") | ||
| last_time = time | ||
| last_block = block | ||
|
|
||
| # Add the function call | ||
| calls.append(f"Tester.{func_name}({params});") | ||
|
|
||
| return calls | ||
|
|
||
| def detect_trace_format(trace): | ||
| """Detect whether the trace is in Echidna or Medusa format.""" | ||
| # Check for Medusa format indicators (block=X, time=Y, sender=0xZ) | ||
| if re.search(r"\(block=\d+,\s*time=\d+.*sender=0x[a-fA-F0-9]+\)", trace): | ||
| return "medusa" | ||
| # Default to Echidna format | ||
| return "echidna" | ||
|
|
||
| def generate_foundry_test(calls, test_name="test_replay"): | ||
| """Generate the Solidity test function code.""" | ||
| test_code = [f"function {test_name}() public {{"] | ||
| test_code.extend(f" {call}" for call in calls) | ||
| test_code.append("}") | ||
|
|
||
| return "\n".join(test_code) | ||
|
|
||
| # Ask user to paste the trace | ||
| print("Paste your Echidna or Medusa call trace below. Press Enter twice to finish:") | ||
| trace = [] | ||
| while True: | ||
| line = input() | ||
| if line: | ||
| trace.append(line.strip()) | ||
| else: | ||
| break | ||
| trace = "\n".join(trace) | ||
|
|
||
| # Detect format and parse the trace | ||
| format_type = detect_trace_format(trace) | ||
| if format_type == "medusa": | ||
| print("\nDetected Medusa trace format") | ||
| parsed_calls = parse_medusa_trace(trace) | ||
| else: | ||
| print("\nDetected Echidna trace format") | ||
| parsed_calls = parse_echidna_trace(trace) | ||
|
|
||
| # Generate the test | ||
| solidity_test = generate_foundry_test(parsed_calls) | ||
|
|
||
| # Output the generated Solidity test | ||
| print("\nGenerated Foundry Test Function:\n") | ||
| print(solidity_test) |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,12 @@ | ||
| // SPDX-License-Identifier: MIT | ||
| pragma solidity ^0.8.19; | ||
|
|
||
| // Handler contracts | ||
| import {HubHandler} from './handlers/HubHandler.t.sol'; | ||
| import {HubConfiguratorHandler} from './handlers/HubConfiguratorHandler.t.sol'; | ||
| import {DonationAttackHandler} from './handlers/simulators/DonationAttackHandler.t.sol'; | ||
|
|
||
| /// @notice Helper contract to aggregate all handler contracts for hub suite | ||
| abstract contract HandlerAggregator is HubHandler, HubConfiguratorHandler, DonationAttackHandler { | ||
| function _setUpHandlers() internal {} | ||
| } |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,53 @@ | ||
| // SPDX-License-Identifier: MIT | ||
| pragma solidity ^0.8.19; | ||
|
|
||
| import {HubInvariants} from './invariants/HubInvariants.t.sol'; | ||
|
|
||
| /// @title Invariants | ||
| /// @notice Aggregator for hub invariants | ||
| abstract contract Invariants is HubInvariants { | ||
| function invariant_INV_HUB() public returns (bool) { | ||
| uint256 assetCount = hub.getAssetCount(); | ||
|
|
||
| for (uint256 i; i < assetCount; i++) { | ||
| // HUB | ||
| assert_INV_HUB_A(i); | ||
| assert_INV_HUB_B(i); | ||
| assert_INV_HUB_C(i); | ||
| assert_INV_HUB_E(i); | ||
| assert_INV_HUB_F(i); | ||
| assert_INV_HUB_GH(i); | ||
| assert_INV_HUB_I(i); | ||
| assert_INV_HUB_K(i); | ||
| assert_INV_HUB_O(i); | ||
| assert_INV_HUB_P(i); | ||
| for (uint256 j; j < NUMBER_OF_ACTORS; j++) { | ||
| assert_INV_HUB_ERC4626_A(i, actorAddresses[j]); | ||
| assert_INV_HUB_ERC4626_B(i, actorAddresses[j]); | ||
| } | ||
| assert_INV_HUB_ERC4626_C(i); | ||
| assert_INV_HUB_ERC4626_D(i); | ||
| } | ||
|
|
||
| return true; | ||
| } | ||
|
|
||
| function invariant_INV_HUB_AVAILABILITY() public returns (bool) { | ||
| uint256 assetCount = hub.getAssetCount(); | ||
| for (uint256 i; i < assetCount; i++) { | ||
| assert_INV_HUB_AVAILABILITY_A(i); | ||
| assert_INV_HUB_AVAILABILITY_B(i); | ||
| assert_INV_HUB_AVAILABILITY_C(i); | ||
| assert_INV_HUB_AVAILABILITY_D(i); | ||
| assert_INV_HUB_AVAILABILITY_E(i); | ||
| for (uint256 j; j < NUMBER_OF_ACTORS; j++) { | ||
| assert_INV_HUB_AVAILABILITY_F(i, actorAddresses[j]); | ||
| assert_INV_HUB_AVAILABILITY_G(i, actorAddresses[j]); | ||
| assert_INV_HUB_AVAILABILITY_H(i, actorAddresses[j]); | ||
| assert_INV_HUB_AVAILABILITY_I(i, actorAddresses[j]); | ||
| } | ||
| } | ||
|
|
||
| return true; | ||
| } | ||
| } |
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.