Creator
Alex North
Created
Feb 8, 2024 9:39 PM
State invariants after FIP-0076
Miner actor
- Sector (DealWeight + VerifiedDealWeight)/(Expiration-PowerBaseEpoch) ≤ SectorSize
- Should already be the case, and checked somewhere
Market actor
- For every DealState, if SlashEpoch ≠ -1, then SectorNumber == 0
- For each DealID→State in DealState, if State.SlashEpoch == -1 and State.EndEpoch > current, then the DealID exists in ProviderSectors[Provider][State.SectorNumber]
- Conversely, the DealID does not exist if State.SlashEpoch ≠ -1
- And the reverse: every ProviderSectors[Provider][SectorNumber]DealID has a corresponding DealState, with SlashEpoch == -1
Between actors
- For each verified claim that has not passed its max term, if the Claim.Sector exists, Claim.Size <= sector VerifiedDealWeight/(Expiration-PowerBaseEpoch)
- Should already be the case and checked
- For each sector, VerifiedDealWeight/(Expiration-PowerBaseEpoch) is the sum of the size of claims that nominate that sector and have not passed their term max
- There is no invariant between DealProposal.verified and existence of verified claims. Allocations/claims may expire unfulfilled, but the deal activated regardless.