Skip to content

Commit

Permalink
Newepch state is up and working.
Browse files Browse the repository at this point in the history
  • Loading branch information
TimSheard committed Apr 30, 2024
1 parent 6a85167 commit b9dd923
Show file tree
Hide file tree
Showing 4 changed files with 259 additions and 162 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -23,8 +23,8 @@ dStateSpec ::
IsConwayUniv fn =>
Specification fn (DState (ConwayEra StandardCrypto))
dStateSpec = constrained $ \ds ->
match ds $ \rewardMap _futureGenDelegs _genDelegs _rewards ->
match rewardMap $ \rdMap ptrMap sPoolMap _dRepMap ->
match ds $ \umap _futureGenDelegs _genDelegs _rewards ->
match umap $ {- \ umapRep -> match umapRep $ -} \rdMap ptrMap sPoolMap _dRepMap ->
[ assertExplain ["dom sPoolMap is a subset of dom rdMap"] $ dom_ sPoolMap `subset_` dom_ rdMap
, assertExplain ["dom ptrMap is empty"] $ dom_ ptrMap ==. mempty
]
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -57,6 +57,7 @@ module Test.Cardano.Ledger.Constrained.Conway.Instances (
gasProposalProcedure_,
protocolVersion_,
maxTxSize_,
-- UMapRep(..),
) where

import Cardano.Chain.Common (
Expand Down Expand Up @@ -123,14 +124,17 @@ import Cardano.Ledger.Shelley.PParams
import Cardano.Ledger.Shelley.PoolRank
import Cardano.Ledger.Shelley.Rules
import Cardano.Ledger.Shelley.TxAuxData (Metadatum)
import Cardano.Ledger.Shelley.TxOut (ShelleyTxOut (..))
import Cardano.Ledger.TxIn (TxId (..), TxIn (..))

-- import Cardano.Ledger.UMap(UMap(..),RDPair(..),UMElem(..))
import Cardano.Ledger.UMap
import Cardano.Ledger.UTxO
import Cardano.Ledger.Val (Val)
import Constrained hiding (Value)
import Constrained qualified as C
import Constrained.Spec.Map
import Constrained.Base (Term (..))
import Constrained.Spec.Map
import Constrained.Univ ()
import Control.Monad.Trans.Fail.String
import Crypto.Hash (Blake2b_224)
Expand Down Expand Up @@ -167,6 +171,7 @@ import System.Random
import Test.Cardano.Ledger.Allegra.Arbitrary ()
import Test.Cardano.Ledger.Alonzo.Arbitrary ()
import Test.Cardano.Ledger.Core.Utils
import Test.Cardano.Ledger.Shelley.Utils
import Test.QuickCheck hiding (Args, Fun, forAll)

type ConwayUnivFns = CoinFn : StringFn : MapFn : FunFn : TreeFn : BaseFns
Expand Down Expand Up @@ -364,6 +369,38 @@ instance IsConwayUniv fn => HasSpec fn Addr28Extra
instance HasSimpleRep DataHash32
instance IsConwayUniv fn => HasSpec fn DataHash32

type ShelleyTxOutTypes era =
'[ Addr (EraCrypto era)
, Value era
]
instance (Era era, Val (Value era)) => HasSimpleRep (ShelleyTxOut era) where
type SimpleRep (ShelleyTxOut era) = SOP '["ShelleyTxOut" ::: ShelleyTxOutTypes era]
toSimpleRep (ShelleyTxOut addr val) =
inject @"ShelleyTxOut" @'["ShelleyTxOut" ::: ShelleyTxOutTypes era]
addr
val
fromSimpleRep rep =
algebra @'["ShelleyTxOut" ::: ShelleyTxOutTypes era] rep ShelleyTxOut

instance (EraTxOut era, HasSpec fn (Value era), IsConwayUniv fn) => HasSpec fn (ShelleyTxOut era)

type AlonzoTxOutTypes era =
'[ Addr (EraCrypto era)
, Value era
, StrictMaybe (DataHash (EraCrypto era))
]
instance (Era era, Val (Value era)) => HasSimpleRep (AlonzoTxOut era) where
type SimpleRep (AlonzoTxOut era) = SOP '["AlonzoTxOut" ::: AlonzoTxOutTypes era]
toSimpleRep (AlonzoTxOut addr val mdat) =
inject @"AlonzoTxOut" @'["AlonzoTxOut" ::: AlonzoTxOutTypes era]
addr
val
mdat
fromSimpleRep rep =
algebra @'["AlonzoTxOut" ::: AlonzoTxOutTypes era] rep AlonzoTxOut

instance (EraTxOut era, HasSpec fn (Value era), IsConwayUniv fn) => HasSpec fn (AlonzoTxOut era)

type BabbageTxOutTypes era =
'[ Addr (EraCrypto era)
, Value era
Expand Down Expand Up @@ -860,22 +897,6 @@ instance
instance HasSimpleRep (Constitution era)
instance (IsConwayUniv fn, EraPParams era) => HasSpec fn (Constitution era)

{-
instance HasSimpleRep (PParamsHKD StrictMaybe era) => HasSimpleRep (PParamsUpdate era) where
type SimpleRep (PParamsUpdate era) = SimpleRep (PParamsHKD StrictMaybe era)
toSimpleRep (PParamsUpdate hkd) = toSimpleRep hkd
fromSimpleRep = PParamsUpdate . fromSimpleRep
instance
( IsConwayUniv fn
, EraPParams era
, HasSimpleRep (PParamsHKD StrictMaybe era)
, TypeSpec fn (SimpleRep (PParamsHKD StrictMaybe era)) ~ TypeSpec fn (PParamsHKD StrictMaybe era)
, HasSpec fn (SimpleRep (PParamsHKD StrictMaybe era))
, Show (TypeSpec fn (PParamsHKD StrictMaybe era))
) =>
HasSpec fn (PParamsUpdate era)
-}

instance HasSimpleRep EpochInterval
instance IsConwayUniv fn => OrdLike fn EpochInterval
instance IsConwayUniv fn => HasSpec fn EpochInterval
Expand All @@ -890,11 +911,6 @@ instance
instance HasSimpleRep (ConwayPParams Identity era)
instance (IsConwayUniv fn, Era era) => HasSpec fn (ConwayPParams Identity era)

{-
instance HasSimpleRep (PParams (ConwayEra StandardCrypto))
instance IsConwayUniv fn => HasSpec fn (PParams (ConwayEra StandardCrypto))
-}

instance HasSimpleRep ExUnits where
type SimpleRep ExUnits = SimpleRep (Natural, Natural)
fromSimpleRep = uncurry ExUnits . fromSimpleRep
Expand Down Expand Up @@ -1027,7 +1043,7 @@ instance (IsConwayUniv fn, Era era) => HasSpec fn (VState era)
instance HasSimpleRep (PState era)
instance (IsConwayUniv fn, Era era) => HasSpec fn (PState era)

instance HasSimpleRep (DState era)
instance Era era => HasSimpleRep (DState era)
instance (IsConwayUniv fn, Era era) => HasSpec fn (DState era)

instance HasSimpleRep (FutureGenDeleg c)
Expand Down Expand Up @@ -1206,6 +1222,35 @@ instance
) =>
HasSpec fn (EpochState era)

instance Crypto c => HasSimpleRep (BlocksMade c)
instance (Crypto c, IsConwayUniv fn) => HasSpec fn (BlocksMade c)

instance HasSimpleRep RewardType
instance IsConwayUniv fn => HasSpec fn RewardType

instance Crypto c => HasSimpleRep (Reward c)
instance (Crypto c, IsConwayUniv fn) => HasSpec fn (Reward c)

instance Crypto c => HasSimpleRep (RewardUpdate c)
instance (Crypto c, IsConwayUniv fn) => HasSpec fn (RewardUpdate c)

instance Crypto c => HasSimpleRep (PulsingRewUpdate c) where
type SimpleRep (PulsingRewUpdate c) = SimpleRep (RewardUpdate c)
toSimpleRep (Complete x) = toSimpleRep x
toSimpleRep x@(Pulsing _ _) = toSimpleRep (runShelleyBase (fst <$> (completeRupd x)))
fromSimpleRep x = Complete (fromSimpleRep x)
instance (Crypto c, IsConwayUniv fn) => HasSpec fn (PulsingRewUpdate c)

instance Era era => HasSimpleRep (NewEpochState era)
instance
( EraTxOut era
, IsConwayUniv fn
, HasSpec fn (TxOut era)
, HasSpec fn (GovState era)
, HasSpec fn (StashedAVVMAddresses era)
) =>
HasSpec fn (NewEpochState era)

instance HasSimpleRep (NonMyopic c)
instance (IsConwayUniv fn, Crypto c) => HasSpec fn (NonMyopic c)

Expand Down

0 comments on commit b9dd923

Please sign in to comment.