diff --git a/plutus-core/plutus-core/src/PlutusCore/Default/Builtins.hs b/plutus-core/plutus-core/src/PlutusCore/Default/Builtins.hs index 4655394dc8d..4604478d300 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Default/Builtins.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Default/Builtins.hs @@ -2071,7 +2071,7 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where (runCostingFunTwoArguments . unimplementedCostingFun) toBuiltinMeaning _semvar ValueContains = - let valueContainsDenotation :: Value -> Value -> Bool + let valueContainsDenotation :: Value -> Value -> BuiltinResult Bool valueContainsDenotation = Value.valueContains {-# INLINE valueContainsDenotation #-} in makeBuiltinMeaning diff --git a/plutus-core/plutus-core/src/PlutusCore/Value.hs b/plutus-core/plutus-core/src/PlutusCore/Value.hs index 7b8f84dd013..fb04b52e121 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Value.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Value.hs @@ -1,6 +1,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE TupleSections #-} {-# LANGUAGE ViewPatterns #-} module PlutusCore.Value ( @@ -9,6 +10,7 @@ module PlutusCore.Value ( k, unK, maxKeyLen, + negativeAmounts, NestedMap, unpack, pack, @@ -34,14 +36,13 @@ import Data.Bitraversable import Data.ByteString (ByteString) import Data.ByteString qualified as B import Data.ByteString.Base64 qualified as Base64 -import Data.Functor -import Data.Hashable (Hashable) +import Data.Hashable (Hashable (..)) import Data.IntMap.Strict (IntMap) import Data.IntMap.Strict qualified as IntMap import Data.Map.Merge.Strict qualified as M import Data.Map.Strict (Map) import Data.Map.Strict qualified as Map -import Data.Maybe +import Data.Monoid (All (..)) import Data.Text.Encoding qualified as Text import GHC.Generics @@ -103,17 +104,25 @@ data Value {- ^ Total size, i.e., sum total of inner map sizes. This avoids recomputing the total size during the costing of operations like `unionValue`. -} + {-# UNPACK #-} !Int + -- ^ The number of negative amounts it contains. deriving stock (Eq, Show, Generic) - deriving anyclass (Hashable, NFData) + deriving anyclass (NFData) + +instance Hashable Value where + hash = hash . unpack + {-# INLINE hash #-} + hashWithSalt salt = hashWithSalt salt . unpack + {-# INLINE hashWithSalt #-} instance CBOR.Serialise Value where - encode (Value v _ _) = CBOR.encode v + encode (Value v _ _ _) = CBOR.encode v {-# INLINE encode #-} decode = pack <$> CBOR.decode {-# INLINE decode #-} instance Flat.Flat Value where - encode (Value v _ _) = Flat.encode v + encode (Value v _ _ _) = Flat.encode v {-# INLINE encode #-} decode = pack <$> Flat.decode {-# INLINE decode #-} @@ -123,7 +132,7 @@ instance Flat.Flat Value where The map is guaranteed to not contain empty inner map or zero amount. -} unpack :: Value -> NestedMap -unpack (Value v _ _) = v +unpack (Value v _ _ _) = v {-# INLINE unpack #-} {-| Pack a map from (currency symbol, token name) to amount into a `Value`. @@ -136,12 +145,13 @@ pack = pack' . normalize -- | Like `pack` but does not normalize. pack' :: NestedMap -> Value -pack' v = Value v sizes size +pack' v = Value v sizes size neg where - (sizes, size) = Map.foldl' alg (mempty, 0) v - alg (ss, s) inner = + (sizes, size, neg) = Map.foldl' alg (mempty, 0, 0) v + alg (ss, s, n) inner = ( IntMap.alter (maybe (Just 1) (Just . (+ 1))) (Map.size inner) ss , s + Map.size inner + , n + Map.size (Map.filter (< 0) inner) ) {-# INLINEABLE pack' #-} @@ -149,16 +159,20 @@ pack' v = Value v sizes size contained in the `Value`. -} totalSize :: Value -> Int -totalSize (Value _ _ size) = size +totalSize (Value _ _ size _) = size {-# INLINE totalSize #-} -- | Size of the largest inner map. maxInnerSize :: Value -> Int -maxInnerSize (Value _ sizes _) = maybe 0 fst (IntMap.lookupMax sizes) +maxInnerSize (Value _ sizes _ _) = maybe 0 fst (IntMap.lookupMax sizes) {-# INLINE maxInnerSize #-} +negativeAmounts :: Value -> Int +negativeAmounts (Value _ _ _ neg) = neg +{-# INLINE negativeAmounts #-} + empty :: Value -empty = Value mempty mempty 0 +empty = Value mempty mempty 0 0 {-# INLINE empty #-} toList :: Value -> [(K, [(K, Integer)])] @@ -189,7 +203,7 @@ instance Pretty Value where the size of the largest inner map. -} insertCoin :: ByteString -> ByteString -> Integer -> Value -> BuiltinResult Value -insertCoin currency token amt v@(Value outer sizes size) +insertCoin currency token amt v@(Value outer sizes size neg) | amt == 0 = pure $ deleteCoin currency token v | otherwise = case (k currency, k token) of (Nothing, _) -> fail $ "insertCoin: invalid currency: " <> show (B.unpack currency) @@ -197,44 +211,62 @@ insertCoin currency token amt v@(Value outer sizes size) (Just ck, Just tk) -> let f :: Maybe (Map K Integer) - -> ( -- Just (old size of inner map) if the total size grows by 1, - -- otherwise Nothing - Maybe Int + -> ( -- Left (old size of inner map) if the total size grows by 1, + -- otherwise, Right (old amount) + Either Int Integer , Maybe (Map K Integer) ) f = \case - Nothing -> (Just 0, Just (Map.singleton tk amt)) + Nothing -> (Left 0, Just (Map.singleton tk amt)) Just inner -> - let (isJust -> exists, inner') = + let (moldAmt, inner') = Map.insertLookupWithKey (\_ _ _ -> amt) tk amt inner - in (if exists then Nothing else Just (Map.size inner), Just inner') - (mold, outer') = Map.alterF f ck outer - (sizes', size') = case mold of - Just old -> (updateSizes old (old + 1) sizes, size + 1) - Nothing -> (sizes, size) - in pure $ Value outer' sizes' size' + in (maybe (Left (Map.size inner)) Right moldAmt, Just inner') + (res, outer') = Map.alterF f ck outer + (sizes', size', neg') = case res of + Left oldSize -> + ( updateSizes oldSize (oldSize + 1) sizes + , size + 1 + , if amt < 0 then neg + 1 else neg + ) + Right oldAmt -> + ( sizes + , size + , if oldAmt < 0 && amt > 0 + then neg - 1 + else + if oldAmt > 0 && amt < 0 + then neg + 1 + else neg + ) + in pure $ Value outer' sizes' size' neg' {-# INLINEABLE insertCoin #-} -- | \(O(\log \max(m, k))\) deleteCoin :: ByteString -> ByteString -> Value -> Value -deleteCoin (UnsafeK -> currency) (UnsafeK -> token) (Value outer sizes size) = - Value outer' sizes' size' +deleteCoin (UnsafeK -> currency) (UnsafeK -> token) (Value outer sizes size neg) = + Value outer' sizes' size' neg' where (mold, outer') = Map.alterF f currency outer - (sizes', size') = case mold of - Just old -> (updateSizes old (old - 1) sizes, size - 1) - Nothing -> (sizes, size) + (sizes', size', neg') = case mold of + Just (oldSize, oldAmt) -> + ( updateSizes oldSize (oldSize - 1) sizes + , size - 1 + , if oldAmt < 0 then neg - 1 else neg + ) + Nothing -> (sizes, size, neg) f :: Maybe (Map K Integer) - -> ( -- Just (old size of inner map) if the total size shrinks by 1, otherwise Nothing - Maybe Int + -> ( -- Just (old size of inner map, old amount) if the total size shrinks by 1, + -- otherwise Nothing + Maybe (Int, Integer) , Maybe (Map K Integer) ) f = \case Nothing -> (Nothing, Nothing) Just inner -> let (amt, inner') = Map.updateLookupWithKey (\_ _ -> Nothing) token inner - in (amt $> Map.size inner, if Map.null inner' then Nothing else Just inner') + in ((Map.size inner,) <$> amt, if Map.null inner' then Nothing else Just inner') -- | \(O(\log \max(m, k))\) lookupCoin :: ByteString -> ByteString -> Value -> Integer @@ -251,18 +283,16 @@ the size of the largest inner map in the first `Value`. @lookup currency token a >= amount@, and if @amount < 0@, then @lookup currency token a == amount@. -} -valueContains :: Value -> Value -> Bool -valueContains v = Map.foldrWithKey' go True . unpack +valueContains :: Value -> Value -> BuiltinResult Bool +valueContains v1 v2 + | negativeAmounts v1 > 0 = fail "valueContains: first value contains negative amounts" + | negativeAmounts v2 > 0 = fail "valueContains: second value contains negative amounts" + | otherwise = BuiltinSuccess . getAll $ Map.foldrWithKey' go mempty (unpack v2) where - go c inner = (&&) (Map.foldrWithKey' goInner True inner) + go c inner = (<>) (Map.foldrWithKey' goInner mempty inner) where - goInner t a2 = - (&&) - ( let a1 = lookupCoin (unK c) (unK t) v - in if a2 > 0 - then a1 >= a2 - else a1 == a2 - ) + goInner t a2 = (<>) (All $ lookupCoin (unK c) (unK t) v1 >= a2) +{-# INLINEABLE valueContains #-} {-| The precise complexity is complicated, but an upper bound is \(O(n_{1} \log n_{2}) + O(m)\), where \(n_{1}\) is the total size of the smaller diff --git a/plutus-core/plutus-core/test/TypeSynthesis/Golden/Signatures/DefaultFun/ValueContains.golden.sig b/plutus-core/plutus-core/test/TypeSynthesis/Golden/Signatures/DefaultFun/ValueContains.golden.sig index 7798d7bac42..64589f394ff 100644 --- a/plutus-core/plutus-core/test/TypeSynthesis/Golden/Signatures/DefaultFun/ValueContains.golden.sig +++ b/plutus-core/plutus-core/test/TypeSynthesis/Golden/Signatures/DefaultFun/ValueContains.golden.sig @@ -1 +1 @@ -Value -> Value -> Bool \ No newline at end of file +Value -> Value -> BuiltinResult Bool \ No newline at end of file diff --git a/plutus-core/plutus-core/test/Value/Spec.hs b/plutus-core/plutus-core/test/Value/Spec.hs index 19259169ad1..3c87c097396 100644 --- a/plutus-core/plutus-core/test/Value/Spec.hs +++ b/plutus-core/plutus-core/test/Value/Spec.hs @@ -29,7 +29,7 @@ prop_packUnpackRoundtrip v = v === V.pack (V.unpack v) -- | Verifies that @pack@ correctly updates the sizes prop_packBookkeeping :: V.NestedMap -> Property -prop_packBookkeeping = checkSizes . V.pack +prop_packBookkeeping = checkBookkeeping . V.pack {-| Verifies that @pack@ preserves @Value@ invariants, i.e., no empty inner map or zero amount. @@ -43,7 +43,7 @@ prop_insertCoinBookkeeping v (ValueAmount amt) = forAll (genShortHex (V.totalSize v)) $ \currency -> forAll (genShortHex (V.totalSize v)) $ \token -> let BuiltinSuccess v' = V.insertCoin (V.unK currency) (V.unK token) amt v - in checkSizes v' + in checkBookkeeping v' -- | Verifies that @insertCoin@ preserves @Value@ invariants prop_insertCoinPreservesInvariants :: Value -> ValueAmount -> Property @@ -109,16 +109,45 @@ prop_deleteCoinIdempotent v0 = BuiltinSuccess v = if V.totalSize v0 > 0 then pure v0 else V.insertCoin "c" "t" 1 v0 fl = V.toFlatList v +prop_deleteCoinBookkeeping :: Value -> Property +prop_deleteCoinBookkeeping v = + conjoin [property (checkBookkeeping v') | v' <- vs] + where + fl = V.toFlatList v + vs = scanr (\(c, t, _) -> V.deleteCoin (V.unK c) (V.unK t)) v fl + +prop_deleteCoinPreservesInvariants :: Value -> Property +prop_deleteCoinPreservesInvariants v = + conjoin [property (checkInvariants v') | v' <- vs] + where + fl = V.toFlatList v + vs = scanr (\(c, t, _) -> V.deleteCoin (V.unK c) (V.unK t)) v fl + +toPositiveValue :: Value -> Value +toPositiveValue = V.pack . fmap (fmap abs) . V.unpack + prop_containsReflexive :: Value -> Property -prop_containsReflexive v = property $ V.valueContains v v +prop_containsReflexive (toPositiveValue -> v) = + property $ case V.valueContains v v of + BuiltinSuccess r -> r + _ -> False prop_containsAfterDeletion :: Value -> Property -prop_containsAfterDeletion v = - conjoin [property (V.valueContains v v') | v' <- vs] +prop_containsAfterDeletion (toPositiveValue -> v) = + conjoin [property (case V.valueContains v v' of BuiltinSuccess r -> r; _ -> False) | v' <- vs] where fl = V.toFlatList v vs = scanr (\(c, t, _) -> V.deleteCoin (V.unK c) (V.unK t)) v fl +prop_containsEnforcesPositivity :: Value -> Property +prop_containsEnforcesPositivity v + | V.negativeAmounts v == 0 = case (V.valueContains v V.empty, V.valueContains V.empty v) of + (BuiltinSuccess{}, BuiltinSuccess{}) -> property True + _ -> property False + | otherwise = case (V.valueContains v V.empty, V.valueContains V.empty v) of + (BuiltinFailure{}, BuiltinFailure{}) -> property True + _ -> property False + prop_flatRoundtrip :: Value -> Property prop_flatRoundtrip v = Flat.unflat (Flat.flat v) === Right v @@ -152,15 +181,18 @@ prop_flatDecodeInvalidToken = let flat = Flat.flat $ Map.singleton c (Map.singleton t (100 :: Integer)) in property . isLeft $ Flat.unflat @Value flat -checkSizes :: Value -> Property -checkSizes v = +checkBookkeeping :: Value -> Property +checkBookkeeping v = (expectedMaxInnerSize === actualMaxInnerSize) .&&. (expectedSize === actualSize) + .&&. (expectedNeg === actualNeg) where expectedMaxInnerSize = fromMaybe 0 . maximumMay $ Map.map Map.size (V.unpack v) actualMaxInnerSize = V.maxInnerSize v expectedSize = sum $ Map.map Map.size (V.unpack v) actualSize = V.totalSize v + expectedNeg = length [amt | inner <- Map.elems (V.unpack v), amt <- Map.elems inner, amt < 0] + actualNeg = V.negativeAmounts v checkInvariants :: Value -> Property checkInvariants (V.unpack -> v) = @@ -228,12 +260,21 @@ tests = , testProperty "deleteCoinIdempotent" prop_deleteCoinIdempotent + , testProperty + "deleteCoinBookkeeping" + prop_deleteCoinBookkeeping + , testProperty + "deleteCoinPreservesInvariants" + prop_deleteCoinPreservesInvariants , testProperty "containsReflexive" prop_containsReflexive , testProperty "containsAfterDeletion" prop_containsAfterDeletion + , testProperty + "containsEnforcesPositivity" + prop_containsEnforcesPositivity , testProperty "unValueDataValidatesCurrency" prop_unValueDataValidatesCurrency diff --git a/plutus-tx/src/PlutusTx/Builtins/Internal.hs b/plutus-tx/src/PlutusTx/Builtins/Internal.hs index 2ed53229c79..d456be62eb8 100644 --- a/plutus-tx/src/PlutusTx/Builtins/Internal.hs +++ b/plutus-tx/src/PlutusTx/Builtins/Internal.hs @@ -1107,7 +1107,12 @@ unionValue (BuiltinValue v1) (BuiltinValue v2) = BuiltinValue $ Value.unionValue {-# OPAQUE unionValue #-} valueContains :: BuiltinValue -> BuiltinValue -> Bool -valueContains (BuiltinValue v1) (BuiltinValue v2) = Value.valueContains v1 v2 +valueContains (BuiltinValue v1) (BuiltinValue v2) = case Value.valueContains v1 v2 of + BuiltinSuccess r -> r + BuiltinSuccessWithLogs logs r -> traceAll logs r + BuiltinFailure logs err -> + traceAll (logs <> pure (display err)) $ + Haskell.error "valueContains errored." {-# OPAQUE valueContains #-} mkValue :: BuiltinValue -> BuiltinData