VoteDelegsVDeleg

{-# OPTIONS --safe #-}

open import Ledger.Conway.Gov.Base

module Ledger.Conway.Certs.Properties.VoteDelegsVDeleg (gs : _) (open GovStructure gs) where

open import Ledger.Conway.Certs gs
open import Ledger.Prelude
open import Ledger.Conway.Gov.Actions gs

- *Informally*. A `CertState`{.AgdaRecord} has a `DState`{.AgdaDatatype}, `PState`{.AgdaDatatype}, and a `GState`{.AgdaDatatype}. The `DState`{.AgdaDatatype} contains a field `voteDelegs`{.AgdaField} which is a mapping from `Credential`{.AgdaDatatype} to `VDeleg`{.AgdaDatatype}. `VDeleg`{.AgdaDatatype} is a datatype with three constructors; the one of interest to us here is `credVoter`{.AgdaInductiveConstructor}, which takes two arguments, a `GovRole`{.AgdaDatatype} and a `Credential`{.AgdaDatatype}. Now suppose we have a collection of credentials—for instance, given : `DState`{.AgdaDatatype}, take to be the domain of the `voteDelegs`{.AgdaField} field of . We could then obtain a set of `VDeleg`{.AgdaDatatype}s by applying `credVoter`{.AgdaInductiveConstructor} `DRep`{.AgdaInductiveConstructor} to each element of . The present property asserts that the set of `VDeleg`{.AgdaDatatype}s that results from the application of `credVoter`{.AgdaInductiveConstructor} `DRep`{.AgdaInductiveConstructor} to the domain of the `voteDelegs`{.AgdaField} of contains the range of the `voteDelegs`{.AgdaField} of . - *Formally*.

voteDelegsVDeleg :  DState → Type
voteDelegsVDeleg d = range (voteDelegsOf d) ⊆ mapˢ (credVoter DRep) (dom (voteDelegsOf d))

- *Proof*. To appear in the module in the [formal ledger repository](\repourl).