Skip to content

Commit

Permalink
Merge pull request #1900 from input-output-hk/ts-add-val-properties
Browse files Browse the repository at this point in the history 
Ts add val properties
  • Loading branch information
Jared Corduan committed Oct 13, 2020
2 parents 262c98f + 2003179 commit 0215b57
Show file tree
Hide file tree
Showing 10 changed files with 634 additions and 272 deletions.
1 change: 1 addition & 0 deletions shelley-ma/impl/cardano-ledger-shelley-ma.cabal
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ library
Cardano.Ledger.Allegra
Cardano.Ledger.Mary
Cardano.Ledger.ShelleyMA.Value
Cardano.Ledger.ShelleyMA.ValueInternal
other-modules:
Cardano.Ledger.ShelleyMA
Cardano.Ledger.ShelleyMA.Timelocks
Expand Down
248 changes: 16 additions & 232 deletions shelley-ma/impl/src/Cardano/Ledger/ShelleyMA/Value.hs
View file
Original file line number Diff line number Diff line change
@@ -1,50 +1,25 @@
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE StandaloneDeriving #-}

-- | The Value module only exports the Value type and its operations 'insert', 'lookup', 'showValue'.
-- Of course Value is an instance of both Val(zero,isZero,(<+>),(<->),(<×>),coin,inject,...) and
-- Albelian(memtpy,(<>)), so one can use those operations as well.
module Cardano.Ledger.ShelleyMA.Value
( Quantity (..),
PolicyID (..),
( PolicyID (..),
AssetID (..),
Value (..),
Value,
insert,
lookup,
showValue,
)
where

import Cardano.Binary
( FromCBOR,
ToCBOR,
encodeListLen,
fromCBOR,
toCBOR,
)
import Cardano.Ledger.Era
import Cardano.Ledger.Val (Val)
import qualified Cardano.Ledger.Val as Val
import Control.DeepSeq (NFData (..))
import Data.ByteString (ByteString)
import Data.Group (Abelian, Group (..))
import Data.Map.Internal
( Map (..),
balanceL,
balanceR,
link,
link2,
singleton,
splitLookup,
import Cardano.Ledger.ShelleyMA.ValueInternal
( AssetID (..),
PolicyID (..),
Value,
insert,
lookup,
showValue,
)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Monoid (Sum (..))
import Data.PartialOrd (PartialOrd)
import Data.Typeable (Typeable)
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))
import Shelley.Spec.Ledger.Coin (Coin (..))
import Shelley.Spec.Ledger.Scripts
import Shelley.Spec.Ledger.Serialization (decodeRecordNamed)
import Prelude hiding (lookup)

-- ============================================================================
-- Multi Assests
Expand Down Expand Up @@ -72,194 +47,3 @@ import Shelley.Spec.Ledger.Serialization (decodeRecordNamed)
-- use 'Ledger.Ada.fromValue'. Plutus contract authors will be able to define
-- modules similar to 'Ledger.Ada' for their own assets.
-- ============================================================================

-- | Quantity
newtype Quantity = Quantity {unInt :: Integer}
deriving newtype
( Show,
Enum,
Eq,
FromCBOR,
NFData,
NoThunks,
Ord,
PartialOrd,
ToCBOR
)
deriving stock
(Generic)
deriving (Semigroup, Monoid, Group, Abelian) via Sum Integer
deriving (Val) via Coin

-- | Asset ID
newtype AssetID = AssetID {assetID :: ByteString}
deriving newtype
( Show,
Eq,
ToCBOR,
FromCBOR,
Ord,
NoThunks,
NFData
)

-- | Policy ID
newtype PolicyID era = PolicyID {policyID :: ScriptHash era}
deriving (Show, Eq, ToCBOR, FromCBOR, Ord, NoThunks, NFData)

-- | The Value representing MultiAssets
data Value era = Value !Coin !(Map (PolicyID era) (Map AssetID Quantity))
deriving (Eq, Show, Generic)

-- TODO make these specific
instance NFData (Value era)

instance NoThunks (Value era)

instance Semigroup (Value era) where
Value c m <> Value c1 m1 =
Value (c <> c1) (unionWithV (unionWithV (<>)) m m1)

instance Monoid (Value era) where
mempty = Value mempty mempty

instance Group (Value era) where
invert (Value c m) = Value (invert c) (mapV (mapV invert) m)

instance Abelian (Value era)

instance PartialOrd (Value era) where
(Value c m) <= (Value c1 m1) =
c Val.<= c1 && pointWise (pointWise (Val.<=)) m m1

instance Era era => Val (Value era) where
scale s (Value c v) = Value (Val.scale s c) (mapV (mapV $ Val.scale s) v)
coin (Value c _) = c
inject c = Value c mempty
size (Value _ v) =
-- add uint for the Coin portion in this size calculation
foldr accum uint v
where
-- add addrHashLen for each Policy ID
accum u ans = foldr accumIns (ans + addrHashLen) u
where
-- add assetIdLen and uint for each asset of that Policy ID
accumIns _ ans1 = ans1 + assetIdLen + uint
-- TODO move these constants somewhere (they are also specified in CDDL)
uint :: Integer
uint = 5

assetIdLen :: Integer
assetIdLen = 32

-- address hash length is always same as Policy ID length
addrHashLen :: Integer
addrHashLen = 28

-- ============================================================================
-- Operations on Map, specialised to comparable `Monoid` values.
-- ============================================================================

-- Pointwise comparison assuming the map is the Default value everywhere except
-- where it is defined
pointWise ::
(Ord k, Eq v, Monoid v) =>
(v -> v -> Bool) ->
Map k v ->
Map k v ->
Bool
pointWise _ Tip Tip = True
pointWise p Tip (m@(Bin _ _ _ _ _)) = all (mempty `p`) m
pointWise p (m@(Bin _ _ _ _ _)) Tip = all (`p` mempty) m
pointWise p m (Bin _ k v2 ls rs) =
case Map.splitLookup k m of
(lm, Just v1, rm) -> p v1 v2 && pointWise p ls lm && pointWise p rs rm
_ -> False

-- The following functions enforce the invariant that mempty is never stored in a
-- Map
insertWithV ::
(Ord k, Eq a, Monoid a) =>
(a -> a -> a) ->
k ->
a ->
Map k a ->
Map k a
insertWithV = go
where
go ::
(Ord k, Eq a, Monoid a) =>
(a -> a -> a) ->
k ->
a ->
Map k a ->
Map k a
go _ !kx x Tip = if x == mempty then Tip else singleton kx x
go f !kx x (Bin sy ky y l r) =
case compare kx ky of
LT -> balanceL ky y (go f kx x l) r
GT -> balanceR ky y l (go f kx x r)
EQ -> if new == mempty then link2 l r else Bin sy kx new l r
where
new = f x y
{-# INLINEABLE insertWithV #-}

unionWithV ::
(Ord k, Eq a, Monoid a) =>
(a -> a -> a) ->
Map k a ->
Map k a ->
Map k a
unionWithV _f t1 Tip = t1
unionWithV f t1 (Bin _ k x Tip Tip) = insertWithV f k x t1
unionWithV f (Bin _ k x Tip Tip) t2 = insertWithV f k x t2
unionWithV _f Tip t2 = t2
unionWithV f (Bin _ k1 x1 l1 r1) t2 = case splitLookup k1 t2 of
(l2, mb, r2) -> case mb of
Nothing ->
if x1 == mempty
then link2 l1l2 r1r2
else link k1 x1 l1l2 r1r2
Just x2 ->
if new == mempty
then link2 l1l2 r1r2
else link k1 new l1l2 r1r2
where
new = (f x1 x2)
where
!l1l2 = unionWithV f l1 l2
!r1r2 = unionWithV f r1 r2
{-# INLINEABLE unionWithV #-}

mapV :: (Ord k, Eq a, Monoid a) => (a -> a) -> Map k a -> Map k a
mapV f m = Map.foldrWithKey accum Map.empty m
where
accum k v ans = if new == mempty then ans else Map.insert k new ans
where
new = f v
{-# INLINEABLE mapV #-}

-- CBOR

-- TODO filter out 0s at deserialization
-- TODO Probably the actual serialization will be of the formal Coin OR Value type
-- Maybe better to make this distinction in the TxOut de/serialization

instance
(Era era) =>
ToCBOR (Value era)
where
toCBOR (Value c v) =
encodeListLen 2
<> toCBOR c
<> toCBOR v

instance
(Era era) =>
FromCBOR (Value era)
where
fromCBOR = do
decodeRecordNamed "Value" (const 2) $ do
c <- fromCBOR
v <- fromCBOR
pure $ Value c v

0 comments on commit 0215b57

Please sign in to comment.