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 vDelegCredential{.AgdaInductiveConstructor}, which takes aCredential`{.AgdaDatatype}.

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 vDelegCredential{.AgdaInductiveConstructor} to each element ofC`{.AgdaBound}.

The present property asserts that the set of VDelegs that results from the application of vDelegCredential 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ˢ vDelegCredential (dom (VoteDelegsOf d))

Proof. (coming soon)