valueContains: enforce no negative amounts in either Value (#7376)

Author: zliu41

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

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,29 +145,34 @@ 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' #-}
 
 {-| Total size, i.e., the number of distinct `(currency symbol, token name)` pairs
 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,52 +203,70 @@ 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)
       (_, Nothing) -> fail $ "insertCoin: invalid token: " <> show (B.unpack token)
       (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

plutus-core/plutus-core/test/TypeSynthesis/Golden/Signatures/DefaultFun/ValueContains.golden.sig

@@ -1 +1 @@
-Value -> Value -> Bool
+Value -> Value -> BuiltinResult Bool

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

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