Properties

Properties

This section presents the properties of the ledger that we have formally proved in Agda or plan to do so in the near future. We indicate in which Agda module each property is formally stated and (possibly) proved. A "Claim" is a property that is not yet proved, while a "Theorem" is one for which we have a formal proof.

Preservation of Value

There are several "preservation of value" proofs throughout this formal specificaition. These can be found in the following modules:

• Ledger.Properties.PoV
• Utxo.Properties.PoV
• Certs.Properties.PoV
• Certs.Properties.PoVLemmas

Invariance Properties

To say that a predicate P is an invariant of a transition rule R means the following: if the rule R relates states s and s' and if P holds at state s, then P holds at state s'.

Examples of invariance properties are found in

• Chain.Properties.CredDepsEqualDomRwds
• Chain.Properties.PParamsWellFormed

Matching Governance Action Deposits

ChainGovDepsMatch, LedgerGovDepsMatch, and EpochGovDepsMatch assert that a certain predicate is an invariant of the CHAIN, LEDGER, and EPOCH rules, respectively.

Given a ledger state s, we focus on deposits in the UTxOState of s that are GovActionDeposits and we compare that set of deposits with the GovActionDeposits of the GovState of s. When these two sets are the same, we write govDepsMatch s and say the govDepsMatch relation holds for s. The formal definition of govDepsMatch is given in Ledger.Properties.

The assertion, "the govDepsMatch relation is an invariant of the LEDGER rule," means the following: if govDepsMatch s and s ⇀⦇ tx ,LEDGER⦈ s', then govDepsMatch s'.

The following are examples of this assertion:

• Chain.Properties.GovDepsMatch
• Ledger.Properties.GovDepsMatch
• Epoch.Properties.GovDepsMatch

Minimum Spending Conditions

A minimum spending condition is proved in Utxo.Properties.MinSpend.

Other Miscellaneous Properties

• Certs.Properties.VoteDelegsVDeleg: The set of VDelegs resulting from the application of credVoter DRep to the domain of the voteDelegs of a DState contains the range of the voteDelegs of that DState.

• Chain.Properties.EpochStep: If cs ⇀⦇ b ,CHAIN⦈ cs' and if the enact states of cs and cs' differ, then the epoch of the slot of b is the successor of the last epoch of cs.

• Epoch.Properties.ConstRwds: The NEWEPOCH rule leaves rewards unchanged.

• Epoch.Properties.NoPropSameDReps: If es is a NewEpochState, and if the GovState of es contains no governance proposals, then the set of activeDReps of es in Epoch e is equal to the set of activeDReps of es in the next epoch.

• Gov.Properties.ChangePPGroup: PParam updates have non-empty groups.