This continues a multi-part series walking through the Ante v0.5 protocol design as well as basic secure smart contract development practices. Check out Part 1, Part 2, and Part 3.

Recall from Part 3 that we want to ensure

is always non-negative and does not grow too large. Our initial fuzz testing results below showed this excess balance (in blue) appears to grow quite slowly over time. Today’s post will explain how we obtained provable bounds (in orange) on the excess balance. As before, we will focus on the Challenger excess balance.

Excess balances accrued over time in a single run of our fuzz test

Characterizing and bounding the excess balance

To analyze the challenger excess balance, we first list all state variables which determine the total challenger balance and each user’s balance:

• challengerInfo.totalAmount(denominated in wei)
• challengerInfo.decayMultiplier
• challengerInfo.userInfo[addr].startAmount(denominated in wei)
• challengerInfo.userInfo[addr].startDecayMultiplier

We then determine all functions in AntePool which modify these variables. We find that all modifications occur through the following operations:

• stake()
• unstake()
• updateDecay(),

where we note that several other functions modify these variables only via updateDecay().

Our analysis (full analysis here) shows that the challenger excess balance is always non-negative and bounded above by the number of calls to these functions. More precisely, we find that

where N_D is the number of calls to updateDecay(), N_S is the number of calls to stake(), N_U is the number of calls to unstake(), and the total amount staked (in wei) is bounded by M·challengerInfo.decayMultiplier at all times.

Remember the challenger excess balance is denominated in wei, so our bound on challenger excess balance is extremely small for reasonable values of parameters. Concretely, if there are 10,000 challengers, each of which calls stake()or unstake() 100 times, updateDecay()is called every minute for 10 years, and the total value in the challenger pool is at most 25M ETH, then this bound would come to 0.0015 ETH.

Proving the bound

Our full proof of the bound is written up here, but we give a flavor of our analysis in this post. Assuming that an Ante Pool is in a state where the bounds hold, we will show that after applying any of the operations stake(), unstake(), and updateDecay() the bounds still hold. When an AntePool is started, the challenger excess balance is 0, so this would imply that the bounds hold at initialization. In this post, let’s see why the updateDecay() operation does not change the fact that challenger excess balance is non-negative.

Suppose that T blocks have passed since the last call to updateDecay(), either directly or through another external function call. The effect of updateDecay() is then to update the challenger state variables as follows:

Updates to challengerInfo state variables after updateDecay()

where we use totalAmount′ and decayMultiplier′ to denote the state after the updateDecay() call.

At this point, the unrounded challenger balance for address addr becomes:

The bound in the last line works because ⌊decayMultiplier⌋ ≤ decayMultiplier

If we sum this balance over all challenger addresses then we obtain:

which shows the challenger excess balance remains non-negative as we hoped!

Of course, we’d like to ensure that updateDecay() still preserves the upper bound, that other operations still preserve both bounds, and that a similar analysis also applies to the Staker side. We invite any interested Ante frens to check out our more formal analysis here.

Conclusion

To try out Ante for yourself, stake or challenge Ante Tests on Ante v0.5 live on Mainnet now. If you’d like to get more involved, you can now write your own Ante Tests or ask your favorite protocols to write and stake their own Ante Tests!

Let us know if you have any questions/comments, follow @AnteFinance on Twitter, and join our Discord for more discussion!