`Semigroup Value` violates associativity law

[Renegatto]

Summary

Instance PlutusTx.Semigroup.Semugroup Plutus.V2.Ledger.Api.Value violates associativity law in relation to PlutusTx.Eq.== and Prelude.==.

If Value were built using only singleton and <> - it holds associativity. But manually Value can be constructed in such way that it fails semigroup assosciativy: Value (fromList xs) where xs contains more than one tuples that has the same CurrencySymbol but tokens with different TokenName. An example: Value (fromList [("",fromList [("",1)]),("",fromList [("a",1)])] Also, Value always holds associativity against on (==) getValue.

Steps to reproduce

Steps to reproduce the behavior:

1. Go to REPL
2. Import PlutusTx.Prelude, Plutus.V1.Ledger.Api
3. Put in those lines:

>>> associative a b c = (a <> b) <> c == a <> (b <> c)
>>> associative mempty  (Value (fromList [("",fromList [("",1)]),("",fromList [("a",1)])])) mempty

4. See False

Expected behavior

Expected that for any terms v1, v2, v3 of type Value following returns True:

(v1 <> v2) <> v3 == v1 <> (v2 <> v3)

Where <> and == is from PlutusTx.Prelude or from Prelude.

System info:

• OS: Ubuntu
• Version 20.04
• 58c093a49eb7a369865e361179d649264fc817a4

Screenshots and attachments

QuickCheck tests:

import QuickCheck qualified as QC
import Plutus.PAB.Arbitrary ()
import Plutus.V2.Ledger.Api qualified as Api
import Prelude qualified
import Prelude ((<$>),(<*>), ($))
import PlutusTx.Prelude qualified

main = do
  let associative :: (a -> a -> Bool) -> (a -> a -> a) -> a -> a -> a -> Bool
      associative (.==.) (.*.) a b c =
        (a .*. (b .*. c)) .==. ((a .*. b) .*. c)
        
      test prop = QC.quickCheckWith QC.stdArgs {QC.maxSuccess = 60000} prop
      
      checkInvalidAgainst f g = test $ associative @Value f g
        
  putStrLn "Value that violates associativity"
  checkInvalidAgainst (Prelude.==) (Prelude.<>) -- Will fail
  checkInvalidAgainst (Prelude.==) (PlutusTx.Prelude.<>) -- Will fail
  checkInvalidAgainst (PlutusTx.Prelude.==) (Prelude.<>) -- Will fail
  checkInvalidAgainst (PlutusTx.Prelude.==) (PlutusTx.Prelude.<>) -- Will fail
  -- Will success but takes long time
  checkInvalidAgainst (\(Api.Value m0) (Api.Value m1) -> m0 Plutus.Prelude.== m1) (PlutusTx.Prelude.<>) 
  
  
  -- A way to generate arbitrary valid Value
  let randValue :: QC.Gen Value
        randValue = PlutusTx.Prelude.mconcat <$> 
          QC.listOf (Value.singleton <$> QC.arbitrary <*> QC.arbitrary <*> QC.arbitrary)
             
      checkValidAgainst f g = test $ associative f g  <$> randValue <*> randValue <*> randValue
            
  putStrLn "Value that holds associativity"
  -- All of those test will succed:
  checkValidAgainst (Prelude.==) (Prelude.<>) 
  checkValidAgainst (Prelude.==) (PlutusTx.Prelude.<>) 
  checkValidAgainst (PlutusTx.Prelude.==) (Prelude.<>) 
  checkValidAgainst (PlutusTx.Prelude.==) (PlutusTx.Prelude.<>) 

[L-as]

Isn't the real issue here that fromList :: [(k, v)] -> Map k v doesn't drop duplicate keys? See the behavior of https://hackage.haskell.org/package/containers-0.6.5.1/docs/Data-Map-Lazy.html#v:fromList for reference.

I'm not sure whether this is worth fixing though.

[effectfully]

@Renegatto thank you very much for the report.

I'm not seeing a bug here.

But manually Value can be constructed in such way that it fails semigroup assosciativy: Value (fromList xs) where xs contains more than one tuples that has the same CurrencySymbol but tokens with different TokenName. An example: Value (fromList [("",fromList [("",1)]),("",fromList [("a",1)])]

Yes, if you manually misconstruct a Value (which is what that fromList does there as explained by @L-as ), it won't behave well.

What worried me though is that in your testing code you seem to be using an Arbitrary Value instance relying on fromList and thus misconstructing the generated Value, however git grep 'Arbitrary\s\+Value' didn't show me such an instance, so I assume it was either removed or written by you.

I'm therefore inclined to close this ticket. @michaelpj please verify my reasoning and close the ticket if you agree.

[michaelpj]

Yes, I agree with this. We perhaps shouldn't expose fromList, but I'm unsure. There is arguably an issue about internal invariants not being maintained somewhere, but I'm not sure exactly where.