Skip to content

Commit

Permalink
[#531] Remove the txid type parameter from UTxO types
Browse files Browse the repository at this point in the history
  • Loading branch information
ruhatch committed Jun 4, 2019
1 parent eda917c commit 06a8fc6
Show file tree
Hide file tree
Showing 10 changed files with 117 additions and 149 deletions.
10 changes: 5 additions & 5 deletions byron/chain/executable-spec/src/Cardano/Spec/Chain/STS/Block.hs
Expand Up @@ -16,7 +16,7 @@ import Control.State.Transition.Generator
import Ledger.Core (Hash(Hash), VKey, Slot, Sig)
import Ledger.Delegation
import Ledger.Update (STag, ProtVer, UProp, Vote)
import Ledger.UTxO (TxWits, TxId, TxIn, TxOut, Wit)
import Ledger.UTxO (TxWits, TxIn, TxOut, Wit)

data BlockHeader
= MkBlockHeader
Expand Down Expand Up @@ -59,7 +59,7 @@ data BlockBody
= BlockBody
{ _bDCerts :: [DCert]
-- ^ Delegation certificates
, _bUtxo :: [TxWits TxId]
, _bUtxo :: [TxWits]
-- ^ UTxO payload
, _bUpdProp :: Maybe UProp
-- ^ Update proposal payload
Expand Down Expand Up @@ -105,9 +105,9 @@ bBodySize = fromIntegral . abstractSize costs
, (typeOf (undefined::ProtVer), 1)
, (typeOf (undefined::DCert), 1)
, (typeOf (undefined::Vote), 1)
, (typeOf (undefined::TxWits TxId), 1)
, (typeOf (undefined::Wit TxId), 1)
, (typeOf (undefined::TxIn TxId), 1)
, (typeOf (undefined::TxWits), 1)
, (typeOf (undefined::Wit), 1)
, (typeOf (undefined::TxIn), 1)
, (typeOf (undefined::TxOut), 1)]

-- | Compute the abstract size (in words) that a block header occupies.
Expand Down
Expand Up @@ -39,7 +39,7 @@ import Ledger.Delegation
, _dSEnvSlot
)
import Ledger.Update (PParams, maxBkSz, UPIState)
import Ledger.UTxO (UTxO, TxId)
import Ledger.UTxO (UTxO)

import Cardano.Spec.Chain.STS.Block

Expand All @@ -49,11 +49,11 @@ instance STS BBODY where
type Environment BBODY =
( PParams
, Epoch
, UTxO TxId
, UTxO
)

type State BBODY =
( UTxOState TxId
( UTxOState
, DIState
, UPIState
)
Expand All @@ -67,7 +67,7 @@ instance STS BBODY where
| InvalidUpdateProposalHash
| BUPIFailure (PredicateFailure BUPI)
| DelegationFailure (PredicateFailure DELEG)
| UTXOWSFailure (PredicateFailure (UTXOWS TxId))
| UTXOWSFailure (PredicateFailure UTXOWS)
deriving (Eq, Show)

initialRules = []
Expand Down Expand Up @@ -97,7 +97,7 @@ instance STS BBODY where
, ds
, b ^. bBody ^. bDCerts
)
utxoSt' <- trans @(UTXOWS TxId) $ TRC
utxoSt' <- trans @UTXOWS $ TRC
( UTxOEnv {utxo0 = utxoGenesis, pps = ppsVal}, utxoSt, b ^. bBody ^. bUtxo )

return $! (utxoSt', ds', us')
Expand All @@ -109,5 +109,5 @@ instance Embed BUPI BBODY where
instance Embed DELEG BBODY where
wrapFailed = DelegationFailure

instance Embed (UTXOWS TxId) BBODY where
instance Embed UTXOWS BBODY where
wrapFailed = UTXOWSFailure
Expand Up @@ -31,7 +31,7 @@ import Ledger.Core
import Ledger.Delegation
import Ledger.Update
import qualified Ledger.Update.Generators as UpdateGen
import Ledger.UTxO (TxId, UTxO)
import Ledger.UTxO (UTxO)

import Cardano.Spec.Chain.STS.Block
import Cardano.Spec.Chain.STS.Rule.BHead
Expand All @@ -45,7 +45,7 @@ data CHAIN
instance STS CHAIN where
type Environment CHAIN =
( Slot -- Current slot
, UTxO TxId
, UTxO
-- Components needed to be able to bootstrap the traces generator. They are
-- not part of the formal spec. These might be removed once we have decided
-- on how do we want to model initial states.
Expand All @@ -58,7 +58,7 @@ instance STS CHAIN where
( Slot
, Seq VKeyGenesis
, Hash
, UTxOState TxId
, UTxOState
, DIState
, UPIState
)
Expand All @@ -71,7 +71,7 @@ instance STS CHAIN where
| PBFTFailure (PredicateFailure PBFT)
| MaximumBlockSize Natural Natural
| LedgerDelegationFailure (PredicateFailure DELEG)
| LedgerUTxOFailure (PredicateFailure (UTXOWS TxId))
| LedgerUTxOFailure (PredicateFailure UTXOWS)
deriving (Eq, Show)

initialRules =
Expand All @@ -92,7 +92,7 @@ instance STS CHAIN where
, Set.empty
, Map.empty
)
utxoSt0 <- trans @(UTXOWS TxId) $ IRC UTxOEnv {utxo0 = utxo0', pps = pps' }
utxoSt0 <- trans @UTXOWS $ IRC UTxOEnv {utxo0 = utxo0', pps = pps' }
ds <- trans @DELEG $ IRC dsenv
return $! ( s0
, ds ^. delegationMap . to Bimap.keys . to fromList
Expand Down Expand Up @@ -151,7 +151,7 @@ instance Embed PBFT CHAIN where
instance Embed DELEG CHAIN where
wrapFailed = LedgerDelegationFailure

instance Embed (UTXOWS TxId) CHAIN where
instance Embed UTXOWS CHAIN where
wrapFailed = LedgerUTxOFailure

genesisHash :: Hash
Expand All @@ -166,7 +166,7 @@ instance HasTrace CHAIN where

initEnvGen = (,,,)
<$> gCurrentSlot
<*> (utxo0 <$> initEnvGen @(UTXOWS TxId))
<*> (utxo0 <$> initEnvGen @UTXOWS)
<*> initEnvGen @DELEG
<*> UpdateGen.pparamsGen
where
Expand Down Expand Up @@ -199,7 +199,7 @@ sigGenChain shouldGenDelegation shouldGenUTxO (_sNow, utxo0, dsEnv, pps) (Slot s
NoGenDelegation -> pure []

utxoPayload <- case shouldGenUTxO of
GenUTxO -> sigGen @(UTXOWS TxId) utxoEnv utxo
GenUTxO -> sigGen @UTXOWS utxoEnv utxo
NoGenUTxO -> pure []

let
Expand Down
Expand Up @@ -14,7 +14,7 @@ import qualified Cardano.Spec.Chain.STS.Block as CBM -- Concrete Block Module
import Ledger.Core
import Ledger.Delegation
import Ledger.Update (ProtVer, UProp, Vote)
import Ledger.UTxO (TxWits, TxId)
import Ledger.UTxO (TxWits)


class BlockHeader h where
Expand All @@ -39,7 +39,7 @@ class BlockBody bb where
-- | Delegation certificates.
bbCerts :: bb -> [DCert]
-- | UTxO payload
bbUtxo :: bb -> [TxWits TxId]
bbUtxo :: bb -> [TxWits]
-- | Update proposal payload
bbUpdProp :: bb -> Maybe UProp
-- | Update votes payload
Expand Down
28 changes: 14 additions & 14 deletions byron/ledger/executable-spec/src/Cardano/Ledger/Spec/STS/UTXO.hs
Expand Up @@ -20,30 +20,30 @@ import Control.State.Transition
, (?!)
, judgmentContext
)
import Data.AbstractSize (HasTypeReps)

import Ledger.Core (Lovelace, (∪), (⊆), (⋪), (◁), dom, range)
import Ledger.GlobalParams (lovelaceCap)
import Ledger.Update (PParams)
import Ledger.UTxO (Tx, UTxO, balance, pcMinFee, txins, txouts, value)

data UTXO id
data UTXO

data UTxOEnv id = UTxOEnv { utxo0 :: UTxO id
, pps :: PParams
} deriving (Eq, Show)
data UTxOEnv = UTxOEnv
{ utxo0 :: UTxO
, pps :: PParams
} deriving (Eq, Show)

data UTxOState id = UTxOState { utxo :: UTxO id
, reserves :: Lovelace
}
deriving (Eq, Show)
data UTxOState = UTxOState
{ utxo :: UTxO
, reserves :: Lovelace
} deriving (Eq, Show)

instance (Ord id, HasTypeReps id) => STS (UTXO id) where
instance STS UTXO where

type Environment (UTXO id) = UTxOEnv id
type State (UTXO id) = UTxOState id
type Signal (UTXO id) = Tx id
data PredicateFailure (UTXO id)
type Environment UTXO = UTxOEnv
type State UTXO = UTxOState
type Signal UTXO = Tx
data PredicateFailure UTXO
= EmptyTxInputs
| FeeTooLow
| IncreasedTotalBalance
Expand Down
39 changes: 17 additions & 22 deletions byron/ledger/executable-spec/src/Cardano/Ledger/Spec/STS/UTXOW.hs
Expand Up @@ -28,13 +28,11 @@ import Control.State.Transition
, wrapFailed
)
import Control.State.Transition.Generator (HasTrace, initEnvGen, sigGen)
import Data.AbstractSize (HasTypeReps)

import Ledger.Core
( Addr(Addr)
, KeyPair(KeyPair)
, VKey
, hash
, keyPair
, mkAddr
, owner
Expand All @@ -44,14 +42,11 @@ import Ledger.Core
import qualified Ledger.Update.Generators as UpdateGen
import Ledger.UTxO
( Tx
, TxId(TxId)
, TxId(TxId)
, TxIn
, TxOut(TxOut)
, TxWits(TxWits)
, UTxO(UTxO)
, Wit(Wit)
, addr
, body
, fromTxOuts
, inputs
Expand All @@ -60,42 +55,42 @@ import qualified Ledger.UTxO.Generators as UTxOGen

import Cardano.Ledger.Spec.STS.UTXO

data UTXOW id
data UTXOW

instance (Ord id, HasTypeReps id) => STS (UTXOW id) where
instance STS UTXOW where

type Environment (UTXOW id) = UTxOEnv id
type State (UTXOW id) = UTxOState id
type Signal (UTXOW id) = TxWits id
data PredicateFailure (UTXOW id)
= UtxoFailure (PredicateFailure (UTXO id))
type Environment UTXOW = UTxOEnv
type State UTXOW = UTxOState
type Signal UTXOW = TxWits
data PredicateFailure UTXOW
= UtxoFailure (PredicateFailure UTXO)
| InsufficientWitnesses
deriving (Eq, Show)

initialRules =
[ do
IRC env <- judgmentContext
trans @(UTXO id) $ IRC env
trans @UTXO $ IRC env
]

transitionRules =
[ do
TRC (env, utxoSt@UTxOState {utxo}, tw) <- judgmentContext
witnessed tw utxo ?! InsufficientWitnesses
utxoSt' <- trans @(UTXO id) $ TRC (env, utxoSt, body tw)
utxoSt' <- trans @UTXO $ TRC (env, utxoSt, body tw)
return utxoSt'
]

-- |Determine if a UTxO input is authorized by a given key.
authTxin :: Ord id => VKey -> TxIn id -> UTxO id -> Bool
authTxin :: VKey -> TxIn -> UTxO -> Bool
authTxin key txin (UTxO utxo) = case Map.lookup txin utxo of
Just (TxOut (Addr pay) _) -> key == pay
_ -> False

-- |Given a ledger state, determine if the UTxO witnesses in a given
-- transaction are sufficient.
-- TODO - should we only check for one witness for each unique input address?
witnessed :: Ord id => TxWits id -> UTxO id -> Bool
witnessed :: TxWits -> UTxO -> Bool
witnessed (TxWits tx wits) utxo =
length wits == length ins && all (isWitness tx utxo) (zip ins wits)
where
Expand All @@ -104,14 +99,14 @@ witnessed (TxWits tx wits) utxo =
verify key tx' sig && authTxin key input unspent


instance (Ord id, HasTypeReps id) => Embed (UTXO id) (UTXOW id) where
instance Embed UTXO UTXOW where
wrapFailed = UtxoFailure

-- | Constant list of addresses intended to be used in the generators.
traceAddrs :: [Addr]
traceAddrs = mkAddr <$> [0 .. 10]

instance HasTrace (UTXOW TxId) where
instance HasTrace UTXOW where
initEnvGen
= UTxOEnv <$> genUTxO <*> UpdateGen.pparamsGen
where
Expand All @@ -120,20 +115,20 @@ instance HasTrace (UTXOW TxId) where
-- All the outputs in the initial UTxO need to refer to some
-- transaction id. Since there are no transactions where these outputs
-- come from we use the hash of the address as transaction id.
pure $ fromTxOuts (TxId . hash . addr) txOuts
pure $ fromTxOuts txOuts

sigGen _e st = do
tx <- UTxOGen.tx traceAddrs (utxo st)
tx <- UTxOGen.genTxFromUTxO traceAddrs (utxo st)
let wits = witnessForTxIn tx (utxo st) <$> inputs tx
pure $ TxWits tx wits

witnessForTxIn :: Ord id => Tx id -> UTxO id -> TxIn id -> Wit id
witnessForTxIn :: Tx -> UTxO -> TxIn -> Wit
witnessForTxIn tx (UTxO utxo) txin =
case Map.lookup txin utxo of
Just (TxOut (Addr pay) _) ->
witnessForTx (keyPair $ owner pay) tx
Nothing ->
error "The generators must ensure that we are spending unspent inputs"

witnessForTx :: KeyPair -> Tx id -> Wit id
witnessForTx :: KeyPair -> Tx -> Wit
witnessForTx (KeyPair sk vk) tx = Wit vk (sign sk tx)

0 comments on commit 06a8fc6

Please sign in to comment.