VoteDelegsVDeleg

{-# OPTIONS --safe #-}

open import Ledger.Conway.Specification.Gov.Base

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

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

Claim (voteDelegs by credVoter constructor).

Informally.

A CertState has a DState, a PState, and a GState. The DState contains a field voteDelegs which is a mapping from Credential to VDeleg.

VDeleg is a datatype with three constructors; the one of interest to us here is credVoter, which takes two arguments, a GovRole and a Credential.

Now suppose we have a collection C of credentials—for instance, given d : DState, take C to be the domain of the voteDelegs field of d. We could then obtain a set of VDelegs by applying credVoter DRep to each element of C.

The present property asserts that the set of VDelegs that results from the application of credVoter DRep to the domain of the voteDelegs of d contains the range of the voteDelegs of d.

Formally.

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

Proof. (coming soon)