FIP-0076 state invariants

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.