Addressed Certora's concern with the weighted average calculation

[jalextowle]

Fixes: #561.

This PR adds a test that verifies that updateWeightedAverage satisfies the property of "computing an average" that Certora mentioned during their review last year. Assuming that $\alpha$ is the current average, $\omega$ is the current total weight, $\delta$ is new value, and $\omega_{\delta}$ is the weight of the new value, we expect the following to hold:

$$ \min(\alpha, \delta) \leq \frac{\alpha \cdot \omega + \delta \cdot \omega_{\delta}}{\omega + \omega_{\delta}} \leq \max(\alpha, \delta) $$

When I initially ran the test, this property did not hold on some of the inputs. Since this is an important property that we want to hold and since it's not very expensive to force to be the case, I went ahead and added an explicit clamp to ensure that the average stays in range.

It's worth noting that this property doesn't hold when removing values from the weighted average, so I left that path unchanged.

[github-actions]

Hyperdrive Gas Benchmark

Benchmark suite	Current: 68712c9	Previous: cb519ad	Deviation	Status
addLiquidity: min	1600 gas	1600 gas	0%	🟰
addLiquidity: avg	65125 gas	66362 gas	-1.8640%	✅
addLiquidity: max	275068 gas	275068 gas	0%	🟰
checkpoint: min	1150 gas	1150 gas	0%	🟰
checkpoint: avg	47823 gas	47685 gas	0.2894%	🚨
checkpoint: max	190992 gas	191154 gas	-0.0847%	✅
closeLong: min	1558 gas	1558 gas	0%	🟰
closeLong: avg	27636 gas	27646 gas	-0.0362%	✅
closeLong: max	148136 gas	148136 gas	0%	🟰
closeShort: min	1549 gas	1549 gas	0%	🟰
closeShort: avg	29947 gas	29957 gas	-0.0334%	✅
closeShort: max	147229 gas	147229 gas	0%	🟰
initialize: min	1538 gas	1538 gas	0%	🟰
initialize: avg	213117 gas	213117 gas	0%	🟰
initialize: max	254775 gas	254775 gas	0%	🟰
openLong: min	1487 gas	1487 gas	0%	🟰
openLong: avg	50251 gas	50100 gas	0.3014%	🚨
openLong: max	184902 gas	184695 gas	0.1121%	🚨
openShort: min	1608 gas	1608 gas	0%	🟰
openShort: avg	49543 gas	49264 gas	0.5663%	🚨
openShort: max	179863 gas	179656 gas	0.1152%	🚨
redeemWithdrawalShares: min	1575 gas	1575 gas	0%	🟰
redeemWithdrawalShares: avg	20044 gas	20406 gas	-1.7740%	✅
redeemWithdrawalShares: max	105972 gas	105972 gas	0%	🟰
removeLiquidity: min	1639 gas	1639 gas	0%	🟰
removeLiquidity: avg	149660 gas	149344 gas	0.2116%	🚨
removeLiquidity: max	323566 gas	323566 gas	0%	🟰

This comment was automatically generated by workflow using github-action-benchmark.

[jrhea]

I'm a little slow here. Does it just fail for really small inputs? I think I see how assertGe(updatedAverage, average.min(delta)); could fail with small inputs due to precision loss. i don't see how the other condition would. just curious if you ran into that.

also, is there a pathological issue with the subtraction path that we need to deal with?

[coveralls]

coverage: 95.169% (+0.1%) from 95.069%
when pulling 68712c9 on jalextowle/certora/weighted-average-safety-concerns
into cb519ad on main.