wip

shelley/chain-and-ledger/executable-spec/src/Cardano/Ledger/Core.hs

@@ -1,4 +1,5 @@
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE TypeFamilies #-}
 
 -- | This module defines core type families which we know to vary from era to
@@ -16,6 +17,8 @@ module Cardano.Ledger.Core
 where
 
 import Data.Kind (Type)
+import Cardano.Binary (FromCBOR (..), ToCBOR (..), Annotator)
+import Data.Typeable (Typeable)
 
 class (Compactible (Value era)) => ValType era where
   type family Value era :: Type
@@ -34,6 +37,17 @@ class (Compactible (Value era)) => ValType era where
 --------------------------------------------------------------------------------
 
 class Compactible a where
-  type CompactForm a :: Type
+  data CompactForm a :: Type
   toCompact :: a -> CompactForm a
   fromCompact :: CompactForm a -> a
+
+
+instance (Compactible a, ToCBOR a) => ToCBOR (CompactForm a) where
+  toCBOR = toCBOR . fromCompact
+
+instance (Compactible a, FromCBOR a) => FromCBOR (CompactForm a) where
+  fromCBOR = toCompact <$> fromCBOR
+
+instance (Typeable a, Compactible a, FromCBOR (Annotator a)) => FromCBOR (Annotator (CompactForm a)) where
+  fromCBOR = (fmap . fmap) toCompact fromCBOR
+

shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/Coin.hs

@@ -66,6 +66,6 @@ instance FromCBOR Coin where
       else cborError $ DecoderErrorCustom "Invalid Coin Value" (pack $ show c)
 
 instance Core.Compactible Coin where
-  type CompactForm Coin = Word64
-  toCompact = fromIntegral . unCoin
-  fromCompact = word64ToCoin
+  newtype CompactForm Coin = CompactCoin Word64
+  toCompact = CompactCoin . fromIntegral . unCoin
+  fromCompact (CompactCoin c) = word64ToCoin c

shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/LedgerState.hs

@@ -419,22 +419,22 @@ data EpochState era = EpochState
   deriving (Generic)
 
 deriving stock instance
-  (Era era, Core.Compactible (Core.Value era), Show (Core.Value era)) =>
+  (Era era, Core.ValType era, Show (Core.Value era)) =>
   Show (EpochState era)
 
 instance NoUnexpectedThunks (EpochState era)
 
 instance (Era era) => NFData (EpochState era)
 
 instance
-  (Era era, Core.Compactible (Core.Value era), ToCBOR (Core.CompactForm (Core.Value era))) =>
+  (Era era, Core.ValType era, ToCBOR (Core.CompactForm (Core.Value era))) =>
   ToCBOR (EpochState era)
   where
   toCBOR (EpochState a s l r p n) =
     encodeListLen 6 <> toCBOR a <> toCBOR s <> toCBOR l <> toCBOR r <> toCBOR p <> toCBOR n
 
 instance
-  (Era era, Core.Compactible (Core.Value era), FromCBOR (Core.CompactForm (Core.Value era))) =>
+  (Era era, Core.ValType era, FromCBOR (Core.CompactForm (Core.Value era))) =>
   FromCBOR (EpochState era)
   where
   fromCBOR = do
@@ -531,20 +531,20 @@ data UTxOState era = UTxOState
   deriving (Generic, NFData)
 
 deriving stock instance
-  (Era era, Core.Compactible (Core.Value era), Show (Core.Value era)) =>
+  (Era era, Core.ValType era, Show (Core.Value era)) =>
   Show (UTxOState era)
 
 instance NoUnexpectedThunks (UTxOState era)
 
 instance
-  (Era era, Core.Compactible (Core.Value era), ToCBOR (Core.CompactForm (Core.Value era))) =>
+  (Era era, Core.ValType era, ToCBOR (Core.CompactForm (Core.Value era))) =>
   ToCBOR (UTxOState era)
   where
   toCBOR (UTxOState ut dp fs us) =
     encodeListLen 4 <> toCBOR ut <> toCBOR dp <> toCBOR fs <> toCBOR us
 
 instance
-  (Era era, Core.Compactible (Core.Value era), FromCBOR (Core.CompactForm (Core.Value era))) =>
+  (Era era, Core.ValType era, FromCBOR (Core.CompactForm (Core.Value era))) =>
   FromCBOR (UTxOState era)
   where
   fromCBOR = do
@@ -575,15 +575,15 @@ data NewEpochState era = NewEpochState
   deriving (Generic)
 
 deriving stock instance
-  (Era era, Core.Compactible (Core.Value era), Show (Core.Value era)) =>
+  (Era era, Core.ValType era, Show (Core.Value era)) =>
   Show (NewEpochState era)
 
 instance (Era era) => NFData (NewEpochState era)
 
 instance NoUnexpectedThunks (NewEpochState era)
 
 instance
-  (Era era, Core.Compactible (Core.Value era), ToCBOR (Core.CompactForm (Core.Value era))) =>
+  (Era era, Core.ValType era, ToCBOR (Core.CompactForm (Core.Value era))) =>
   ToCBOR (NewEpochState era)
   where
   toCBOR (NewEpochState e bp bc es ru pd os) =
@@ -593,7 +593,7 @@ instance
       <> toCBOR os
 
 instance
-  (Era era, Core.Compactible (Core.Value era), FromCBOR (Core.CompactForm (Core.Value era))) =>
+  (Era era, Core.ValType era, FromCBOR (Core.CompactForm (Core.Value era))) =>
   FromCBOR (NewEpochState era)
   where
   fromCBOR = do
@@ -634,22 +634,22 @@ data LedgerState era = LedgerState
   deriving (Generic)
 
 deriving stock instance
-  (Era era, Core.Compactible (Core.Value era), Show (Core.Value era)) =>
+  (Era era, Core.ValType era, Show (Core.Value era)) =>
   Show (LedgerState era)
 
 instance NoUnexpectedThunks (LedgerState era)
 
 instance (Era era) => NFData (LedgerState era)
 
 instance
-  (Era era, Core.Compactible (Core.Value era), ToCBOR (Core.CompactForm (Core.Value era))) =>
+  (Era era, Core.ValType era, ToCBOR (Core.CompactForm (Core.Value era))) =>
   ToCBOR (LedgerState era)
   where
   toCBOR (LedgerState u dp) =
     encodeListLen 2 <> toCBOR u <> toCBOR dp
 
 instance
-  (Era era, Core.Compactible (Core.Value era), FromCBOR (Core.CompactForm (Core.Value era))) =>
+  (Era era, Core.ValType era, FromCBOR (Core.CompactForm (Core.Value era))) =>
   FromCBOR (LedgerState era)
   where
   fromCBOR = do
@@ -684,7 +684,7 @@ txsize = fromIntegral . BSL.length . txFullBytes
 -- | It can be helpful for coin selection.
 txsizeBound ::
   forall era.
-  (Era era, Core.Compactible (Core.Value era), ToCBOR (Core.CompactForm (Core.Value era))) =>
+  (Era era, Core.ValType era, ToCBOR (Core.CompactForm (Core.Value era))) =>
   Tx era ->
   Integer
 txsizeBound tx = numInputs * inputSize + numOutputs * outputSize + rest
@@ -710,7 +710,7 @@ minfee pp tx = Coin $ fromIntegral (_minfeeA pp) * txsize tx + fromIntegral (_mi
 -- | Minimum fee bound using txsizeBound
 minfeeBound ::
   forall era.
-  (Era era, Core.Compactible (Core.Value era), ToCBOR (Core.CompactForm (Core.Value era))) =>
+  (Era era, Core.ValType era, ToCBOR (Core.CompactForm (Core.Value era))) =>
   PParams ->
   Tx era ->
   Coin
@@ -721,7 +721,7 @@ minfeeBound pp tx =
 
 -- | Compute the lovelace which are created by the transaction
 produced ::
-  (Era era, Core.Compactible (Core.Value era), Val.Val (Core.Value era), ToCBOR (Core.CompactForm (Core.Value era))) =>
+  (Era era, Core.ValType era, Val.Val (Core.Value era), ToCBOR (Core.CompactForm (Core.Value era))) =>
   PParams ->
   Map (KeyHash 'StakePool era) (PoolParams era) ->
   TxBody era ->
@@ -731,7 +731,7 @@ produced pp stakePools tx =
 
 -- | Compute the key deregistration refunds in a transaction
 keyRefunds ::
-  (Era era, Core.Compactible (Core.Value era), ToCBOR (Core.CompactForm (Core.Value era))) =>
+  (Era era, Core.ValType era, ToCBOR (Core.CompactForm (Core.Value era))) =>
   PParams ->
   TxBody era ->
   Coin
@@ -742,7 +742,7 @@ keyRefunds pp tx = Val.scale (length deregistrations) (_keyDeposit pp)
 -- | Compute the lovelace which are destroyed by the transaction
 -- TODO this is only correct for Shelley!
 consumed ::
-  (Era era, Core.Compactible (Core.Value era), Val.Val (Core.Value era), ToCBOR (Core.CompactForm (Core.Value era))) =>
+  (Era era, Core.ValType era, Val.Val (Core.Value era), ToCBOR (Core.CompactForm (Core.Value era))) =>
   PParams ->
   UTxO (era) ->
   TxBody (era) ->
@@ -784,8 +784,8 @@ witsFromWitnessSet (WitnessSet aWits _ bsWits) =
 witsVKeyNeeded ::
   forall era.
   ( Era era,
-    Core.Compactible (Core.Value era),
-    ToCBOR (Core.CompactForm (Core.Value era))
+    Core.ValType era,
+    ToCBOR (Core.Value era)
   ) =>
   UTxO era ->
   Tx era ->
@@ -873,7 +873,7 @@ propWits (Just (Update (ProposedPPUpdates pup) _)) (GenDelegs genDelegs) =
 
 -- | Calculate the change to the deposit pool for a given transaction.
 depositPoolChange ::
-  (Era era, Core.Compactible (Core.Value era), ToCBOR (Core.CompactForm (Core.Value era))) =>
+  (Era era, Core.ValType era, ToCBOR (Core.CompactForm (Core.Value era))) =>
   LedgerState era ->
   PParams ->
   TxBody era ->
@@ -904,7 +904,7 @@ reapRewards dStateRewards withdrawals =
 
 stakeDistr ::
   forall era.
-  ( (Core.Compactible (Core.Value era)),
+  ( Core.ValType era,
     Val.Val (Core.Value era)
   ) =>
   Era era =>

shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Snap.hs

@@ -3,6 +3,7 @@
 {-# LANGUAGE EmptyDataDeriving #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE TypeFamilies #-}
 
 module Shelley.Spec.Ledger.STS.Snap
@@ -38,7 +39,7 @@ data SnapPredicateFailure era -- No predicate failures
 
 instance NoUnexpectedThunks (SnapPredicateFailure era)
 
-instance (Era era, Core.Compactible (Core.Value era)) => STS (SNAP era) where
+instance (Era era, Core.ValType era, (Val.Val (Core.Value era))) => STS (SNAP era) where
   type State (SNAP era) = SnapShots era
   type Signal (SNAP era) = ()
   type Environment (SNAP era) = LedgerState era
@@ -49,9 +50,8 @@ instance (Era era, Core.Compactible (Core.Value era)) => STS (SNAP era) where
 
 snapTransition ::
   ( Era era,
-    Core.Compactible (Core.Value era),
-    Environment (SNAP era) ~ LedgerState era,
-    State (SNAP era) ~ SnapShots era
+    Core.ValType era,
+    (Val.Val (Core.Value era))
   ) =>
   TransitionRule (SNAP era)
 snapTransition = do

shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxo.hs

@@ -30,7 +30,6 @@ import Cardano.Binary
 import qualified Cardano.Ledger.Core as Core
 import Cardano.Ledger.Crypto (Crypto)
 import Cardano.Ledger.Era (Era)
-import Cardano.Ledger.Shelley (Shelley)
 import qualified Cardano.Ledger.Val as Val
 import Cardano.Prelude (NoUnexpectedThunks (..), asks)
 import Control.Iterate.SetAlgebra (dom, eval, (∪), (⊆), (⋪))
@@ -123,8 +122,8 @@ data UtxoPredicateFailure era
       !Coin -- the minimum fee for this transaction
       !Coin -- the fee supplied in this transaction
   | ValueNotConservedUTxO
-      !Coin -- the Coin consumed by this transaction
-      !Coin -- the Coin produced by this transaction
+      !(Core.Value era) -- the Coin consumed by this transaction
+      !(Core.Value era) -- the Coin produced by this transaction
   | WrongNetwork
       !Network -- the expected network id
       !(Set (Addr era)) -- the set of addresses with incorrect network IDs
@@ -237,14 +236,14 @@ instance
         k -> invalidKey k
 
 instance
-  (Crypto c) =>
-  STS (UTXO (Shelley c))
+  (Era era, Core.ValType era, Val.Val (Core.Value era)) =>
+  STS (UTXO era)
   where
-  type State (UTXO (Shelley c)) = UTxOState (Shelley c)
-  type Signal (UTXO (Shelley c)) = Tx (Shelley c)
-  type Environment (UTXO (Shelley c)) = UtxoEnv (Shelley c)
-  type BaseM (UTXO (Shelley c)) = ShelleyBase
-  type PredicateFailure (UTXO (Shelley c)) = UtxoPredicateFailure (Shelley c)
+  type State (UTXO era) = UTxOState era
+  type Signal (UTXO era) = Tx era
+  type Environment (UTXO era) = UtxoEnv era
+  type BaseM (UTXO era) = ShelleyBase
+  type PredicateFailure (UTXO era) = UtxoPredicateFailure era
 
   transitionRules = [utxoInductive]
   initialRules = [initialLedgerState]
@@ -266,24 +265,25 @@ instance
       PostCondition
         "Deposit pot must not be negative (post)"
         (\_ st' -> _deposited st' >= mempty),
-      let utxoBalance us = _deposited us <> _fees us <> balance (_utxo us)
-          withdrawals txb = foldl' (<>) mempty $ unWdrl $ _wdrls txb
+      let utxoBalance us = (Val.inject $ _deposited us <> _fees us) <> balance (_utxo us)
+          withdrawals :: TxBody era -> Core.Value era
+          withdrawals txb = Val.inject $ foldl' (<>) mempty $ unWdrl $ _wdrls txb
        in PostCondition
             "Should preserve ADA in the UTxO state"
             ( \(TRC (_, us, tx)) us' ->
                 utxoBalance us <> withdrawals (_body tx) == utxoBalance us'
             )
     ]
 
-initialLedgerState :: InitialRule (UTXO (Shelley c))
+initialLedgerState :: InitialRule (UTXO era)
 initialLedgerState = do
   IRC _ <- judgmentContext
   pure $ UTxOState (UTxO Map.empty) (Coin 0) (Coin 0) emptyPPUPState
 
 utxoInductive ::
   forall c era.
-  (Era era, era ~ Shelley c) =>
-  TransitionRule (UTXO (Shelley c))
+  (Era era, Core.ValType era, Val.Val (Core.Value era)) =>
+  TransitionRule (UTXO era)
 utxoInductive = do
   TRC (UtxoEnv slot pp stakepools genDelegs, u, tx) <- judgmentContext
   let UTxOState utxo deposits' fees ppup = u
@@ -320,7 +320,7 @@ utxoInductive = do
 
   let outputs = Map.elems $ unUTxO (txouts txb)
       minUTxOValue = _minUTxOValue pp
-      outputsTooSmall = [out | out@(TxOut _ c) <- outputs, c < (Val.scaledMinDeposit c minUTxOValue)]
+      outputsTooSmall = [out | out@(TxOut _ c) <- outputs, c Val.< (Val.inject $ Val.scaledMinDeposit c minUTxOValue)]
   null outputsTooSmall ?! OutputTooSmallUTxO outputsTooSmall
 
   -- Bootstrap (i.e. Byron) addresses have variable sized attributes in them.
@@ -346,7 +346,7 @@ utxoInductive = do
       }
 
 instance
-  Crypto c =>
-  Embed (PPUP (Shelley c)) (UTXO (Shelley c))
+  (Era era, Core.ValType era) =>
+  Embed (PPUP era) (UTXO era)
   where
   wrapFailed = UpdateFailure

shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/UTxO.hs

@@ -268,7 +268,7 @@ getKeyHashFromRegPool (DCertPool (RegPool p)) = Just . _poolPubKey $ p
 getKeyHashFromRegPool _ = Nothing
 
 txup ::
-  (Era era, Core.ValType era, ToCBOR (Core.CompactForm (Core.Value era))) =>
+  (Era era, Core.ValType era, ToCBOR (Core.Value era)) =>
   Tx era ->
   Maybe (Update era)
 txup (Tx txbody _ _) = strictMaybeToMaybe (_txUpdate txbody)
@@ -298,7 +298,7 @@ scriptCred (ScriptHashObj hs) = Just hs
 scriptsNeeded ::
   ( Era era,
     Core.ValType era,
-    ToCBOR (Core.CompactForm (Core.Value era))
+    ToCBOR (Core.Value era)
   ) =>
   UTxO era ->
   Tx era ->