Closed 0x-r4bbit closed 1 month ago
We now have a bunch of different spec files for certora that all run individually on CI. Some of these files rely on functions and helpers that had to be redefined in multiple places.
To give some examples:
getAccountBalance() https://github.com/logos-co/staking/blob/9f3df7bb242093ebf43097fdd0563148c218a5b4/certora/specs/StakeVault.spec#L20 https://github.com/logos-co/staking/blob/9f3df7bb242093ebf43097fdd0563148c218a5b4/certora/specs/StakeManager.spec#L19 https://github.com/logos-co/staking/blob/9f3df7bb242093ebf43097fdd0563148c218a5b4/certora/specs/StakeManagerStartMigration.spec#L23
mulDivSummary() https://github.com/logos-co/staking/blob/9f3df7bb242093ebf43097fdd0563148c218a5b4/certora/specs/StakeVault.spec#L15 https://github.com/logos-co/staking/blob/9f3df7bb242093ebf43097fdd0563148c218a5b4/certora/specs/StakeManager.spec#L14
isMigrationFunction() (this one can probably be split up further https://github.com/logos-co/staking/blob/9f3df7bb242093ebf43097fdd0563148c218a5b4/certora/specs/StakeVault.spec#L27 https://github.com/logos-co/staking/blob/9f3df7bb242093ebf43097fdd0563148c218a5b4/certora/specs/StakeManager.spec#L47
simplification() (this one we need to check if it can be steamlined safely https://github.com/logos-co/staking/blob/9f3df7bb242093ebf43097fdd0563148c218a5b4/certora/specs/StakeVault.spec#L73 https://github.com/logos-co/staking/blob/9f3df7bb242093ebf43097fdd0563148c218a5b4/certora/specs/StakeManager.spec#L55
requiresPreviousManager() https://github.com/logos-co/staking/blob/9f3df7bb242093ebf43097fdd0563148c218a5b4/certora/specs/StakeManager.spec#L61 https://github.com/logos-co/staking/blob/9f3df7bb242093ebf43097fdd0563148c218a5b4/certora/specs/StakeManagerProcessAccount.spec#L31
requiresNextManager() https://github.com/logos-co/staking/blob/9f3df7bb242093ebf43097fdd0563148c218a5b4/certora/specs/StakeManager.spec#L67 https://github.com/logos-co/staking/blob/9f3df7bb242093ebf43097fdd0563148c218a5b4/certora/specs/StakeManagerProcessAccount.spec#L37
We should find a way to have these streamlined, and then shared in different places without maintaining multiple definitions.
We now have a bunch of different spec files for certora that all run individually on CI. Some of these files rely on functions and helpers that had to be redefined in multiple places.
To give some examples:
getAccountBalance() https://github.com/logos-co/staking/blob/9f3df7bb242093ebf43097fdd0563148c218a5b4/certora/specs/StakeVault.spec#L20 https://github.com/logos-co/staking/blob/9f3df7bb242093ebf43097fdd0563148c218a5b4/certora/specs/StakeManager.spec#L19 https://github.com/logos-co/staking/blob/9f3df7bb242093ebf43097fdd0563148c218a5b4/certora/specs/StakeManagerStartMigration.spec#L23
mulDivSummary() https://github.com/logos-co/staking/blob/9f3df7bb242093ebf43097fdd0563148c218a5b4/certora/specs/StakeVault.spec#L15 https://github.com/logos-co/staking/blob/9f3df7bb242093ebf43097fdd0563148c218a5b4/certora/specs/StakeManager.spec#L14
isMigrationFunction() (this one can probably be split up further https://github.com/logos-co/staking/blob/9f3df7bb242093ebf43097fdd0563148c218a5b4/certora/specs/StakeVault.spec#L27 https://github.com/logos-co/staking/blob/9f3df7bb242093ebf43097fdd0563148c218a5b4/certora/specs/StakeManager.spec#L47
simplification() (this one we need to check if it can be steamlined safely https://github.com/logos-co/staking/blob/9f3df7bb242093ebf43097fdd0563148c218a5b4/certora/specs/StakeVault.spec#L73 https://github.com/logos-co/staking/blob/9f3df7bb242093ebf43097fdd0563148c218a5b4/certora/specs/StakeManager.spec#L55
requiresPreviousManager() https://github.com/logos-co/staking/blob/9f3df7bb242093ebf43097fdd0563148c218a5b4/certora/specs/StakeManager.spec#L61 https://github.com/logos-co/staking/blob/9f3df7bb242093ebf43097fdd0563148c218a5b4/certora/specs/StakeManagerProcessAccount.spec#L31
requiresNextManager() https://github.com/logos-co/staking/blob/9f3df7bb242093ebf43097fdd0563148c218a5b4/certora/specs/StakeManager.spec#L67 https://github.com/logos-co/staking/blob/9f3df7bb242093ebf43097fdd0563148c218a5b4/certora/specs/StakeManagerProcessAccount.spec#L37
We should find a way to have these streamlined, and then shared in different places without maintaining multiple definitions.