logo
Formal Ledger Specification
NoPropSameDReps
Initializing search
    GitHub
    • Navigation
    GitHub
      • Home
      • Guide for Contributors
        • Notation
      • Ledger
        • Prelude
        • Introduction
        • Properties
          • Base
            • HSTypes
            • Util
          • HasCoin
          • Instances
          • Numeric
            • PositiveNat
            • UnitInterval
            • Address
            • Crypto
            • Epoch
        • Conway
          • Specification
            • Abstract
            • BlockBody
              • Properties
            • Certs
              • Properties
                • PoV
                • PoVLemmas
                • VoteDelegsVDeleg
            • Chain
              • Properties
                • CredDepsEqualDomRwds
                • EpochStep
                • GovDepsMatch
                • PParamsWellFormed
            • Enact
              • Properties
            • Epoch
              • Properties
                • ConstRwds
                • GovDepsMatch
                • NoPropSameDReps
            • Fees
            • Gov
              • Base
              • Actions
              • Properties
                • ChangePPGroup
            • Ledger.Ledger
              • Properties
                • GovDepsMatch
                • PoV
            • PoolReap
            • PParams
            • Properties
            • Ratify
              • Properties
            • Rewards
            • RewardUpdate
              • Properties
            • Script
              • Base
              • Timelock
              • Validation
              • Base
              • Coin
              • ValueSet
              • ValueVector
            • Transaction
            • Utxo
              • Properties
                • MinSpend
                • PoV
            • Utxow
              • Properties
              • Examples
                • HelloWorld
                • SucceedIfNumber
              • LedgerImplementation
              • Lib
              • Prelude
              • StructuredContracts
              • GovStructure
            • ConwayBootstrap
            • ConwayBootstrapEnact
            • ExternalFunctions
            • HSLedger
              • Address
              • BaseTypes
              • Cert
              • Certs
              • Chain
              • Core
              • Enact
              • Epoch
              • ExternalStructures
              • Gov
                • Core
                • Actions
              • Ledger
              • NewEpoch
              • PParams
              • Ratify
              • Rewards
              • Transaction
              • Utxo
          • Conformance
            • Certs
              • Properties
            • Chain
              • Properties
            • Epoch
              • Properties
            • Equivalence
              • Bisimilarity
              • Certs
              • Convert
              • Deposits
              • Map
              • Utxo
            • Gov
            • Ledger
              • Properties
            • Properties
            • Rewards
            • Script
            • Utxo
              • Properties
            • Utxow
              • Properties
        • PreConway
            • NewPP
              • Properties
            • PPUp
              • Properties
          • NewPP
            • Properties
          • PPUp
            • Properties
        • Convertible
          • Deriving
          • DerivingTest
        • HaskellTypes
          • Deriving
        • Definitions
        • Agda Prelude
            • ComputationalRelation
            • HasSubset
            • HasSubtract
              • Instance
            • Hashable
            • STS
          • MyDebugOptions

    NoPropSameDReps

    {-# OPTIONS --safe #-}
    
    open import Ledger.Conway.Specification.Transaction
    open import Ledger.Conway.Specification.Abstract
    
    module Ledger.Conway.Specification.Epoch.Properties.NoPropSameDReps
      (txs : _) (open TransactionStructure txs)
      (abs : AbstractFunctions txs) (open AbstractFunctions abs)
      where
    
    open import Ledger.Conway.Specification.Epoch txs abs
    open import Ledger.Conway.Specification.Gov txs
    open import Ledger.Prelude
    open import Ledger.Conway.Specification.Properties txs abs
    

    Claim (DReps unchanged if no gov proposals).

    Informally.

    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.

    Formally.

    prop≡∅⇒activeDReps-const : Epoch → NewEpochState → Type
    prop≡∅⇒activeDReps-const e es =
      GovStateOf es ≡ [] → activeDReps e es ≡ᵉ activeDReps (sucᵉ e) es
    

    Proof. (coming soon)

    Previous
    GovDepsMatch
    Next
    Fees
    Made with Material for MkDocs