leftovers

nivcertora · nivcertora · commit 03d71d9ac7b6 · 2024-03-05T09:55:31.000+02:00
diff --git a/DEFI/LiquidityPool/certora/specs/Full.spec b/DEFI/LiquidityPool/certora/specs/Full.spec
@@ -321,7 +321,7 @@ ghost mathint sumOfShares {
     init_state axiom sumOfShares == 0;
 }
 
-hook Sstore _balanceOf[KEY address user] uint256 newSharesBalance (uint256 oldSharesBalance) STORAGE
+hook Sstore _balanceOf[KEY address user] uint256 newSharesBalance (uint256 oldSharesBalance)
 {
     sumOfShares = sumOfShares + newSharesBalance - oldSharesBalance;
 }
@@ -340,8 +340,7 @@ ghost mathint sumBalances {
     init_state axiom sumBalances == 0;
 }
 
-hook Sstore underlying._balanceOf[KEY address user] uint256 newBalance (uint256 oldBalance) STORAGE
-{
+hook Sstore underlying._balanceOf[KEY address user] uint256 newBalance (uint256 oldBalance) {
     sumBalances = sumBalances + newBalance - oldBalance;
 }
 

Original file line number	Diff line number	Diff line change
`@@ -321,7 +321,7 @@ ghost mathint sumOfShares {`
`321`	`321`	`init_state axiom sumOfShares == 0;`
`322`	`322`	`}`
`323`	`323`
`324`		`-hook Sstore _balanceOf[KEY address user] uint256 newSharesBalance (uint256 oldSharesBalance) STORAGE`
	`324`	`+hook Sstore _balanceOf[KEY address user] uint256 newSharesBalance (uint256 oldSharesBalance)`
`325`	`325`	`{`
`326`	`326`	`sumOfShares = sumOfShares + newSharesBalance - oldSharesBalance;`
`327`	`327`	`}`
`@@ -340,8 +340,7 @@ ghost mathint sumBalances {`
`340`	`340`	`init_state axiom sumBalances == 0;`
`341`	`341`	`}`
`342`	`342`
`343`		`-hook Sstore underlying._balanceOf[KEY address user] uint256 newBalance (uint256 oldBalance) STORAGE`
`344`		`-{`
	`343`	`+hook Sstore underlying._balanceOf[KEY address user] uint256 newBalance (uint256 oldBalance) {`
`345`	`344`	`sumBalances = sumBalances + newBalance - oldBalance;`
`346`	`345`	`}`
`347`	`346`