Skip to content

VoteDelegsVDeleg

Claim: voteDelegs field values are VDelegs constructed from their keys

{-# 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

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, which takes 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 vDelegCredential to each element of C.

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)