Verification staking reward

[shoham-certora]

Initial spec for StakingRewardStream and mutations.

[kasperpawlowski]

it seems that earned1Late == earned1 && earned2Late == earned2 which implies diff1 == diff2 == 0. I guess it should be done as follows instead:

uint256 earned1 = earnedReward(e1, staker1, rewarded, reward, forfeitRecentReward);
uint256 earned2 = earnedReward(e2, staker1, rewarded, reward, forfeitRecentReward);

require e2.block.timestamp > e1.block.timestamp;
uint256 earned1Late = earnedReward(e2, staker1, rewarded, reward, forfeitRecentReward);
uint256 earned2Late = earnedReward(e2, staker2, rewarded, reward, forfeitRecentReward);

[nd-certora]

yes agree it was wrong. Proving the assertion requires first proving some other properties on the reward calculation. So change for now to only satisfy