Fix certora spec. Starting with an invalid state would result in an i…

…nvalid state
OriginProtocol · Jan 7, 2025 · 18d4a51 · 18d4a51
1 parent 07b3e70
commit 18d4a51
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 1 deletion.
diff --git a/certora/specs/OUSD/OtherInvariants.spec b/certora/specs/OUSD/OtherInvariants.spec
@@ -151,10 +151,13 @@ rule changeSupplyIntegrity(uint256 newTotalSupply) {
 	requireInvariant sumAllRebasingCreditsEqRebasingCredits();
 	require OUSD.rebasingCreditsPerToken_ >= e18();
 	require newTotalSupply >= OUSD.totalSupply();
+	/// If garbage in, then garbage out
+	require (nonRebasingSupply() + (rebasingCreditsHighres() / OUSD.rebasingCreditsPerToken_)) <= OUSD.totalSupply();
+	require OUSD.totalSupply() < MAX_TOTAL_SUPPLY();
 
 	OUSD.changeSupply(e, newTotalSupply);
 
-	assert OUSD.totalSupply() == newTotalSupply;
+	assert newTotalSupply < MAX_TOTAL_SUPPLY() ? OUSD.totalSupply() == newTotalSupply : OUSD.totalSupply == MAX_TOTAL_SUPPLY();
 	assert (nonRebasingSupply() + (rebasingCreditsHighres() / OUSD.rebasingCreditsPerToken_)) <= OUSD.totalSupply();
 }
 

diff --git a/certora/specs/OUSD/common.spec b/certora/specs/OUSD/common.spec
@@ -31,6 +31,7 @@ methods {
 definition e18() returns uint256 = 1000000000000000000; // definition for 1e18 
 
 definition MIN_TOTAL_SUPPLY() returns mathint = 10^16;
+definition MAX_TOTAL_SUPPLY() returns mathint = 2^128 - 1;
 
 // RebaseOptions state definitions
 definition NotSet() returns OUSD.RebaseOptions = OUSD.RebaseOptions.NotSet;