Make the unionWith property test differential against the builtin

Compare the typed unionWith (+) against the builtin unionValue path on
CEK rather than against host-Haskell unionWith: a shared-source oracle
cannot catch a bug that lands the same way on both sides. Inputs are
restricted to the well-formed domain unsafeDataAsValue accepts, and
results are compared up to key order and zero-sum entries. Bindings use
plinthc instead of the compile splice.

Also rephrase Note [Single-pass unionWith] and the checkBinRel docstring
to describe the present structure without contrasting against history.

For IntersectMBO/plutus-private#2243.

Author: Unisay

plutus-ledger-api/src/PlutusLedgerApi/V1/Data/Value.hs

@@ -402,20 +402,12 @@ assetClassValueOf :: Value -> AssetClass -> Integer
 assetClassValueOf v (AssetClass (c, t)) = valueOf v c t
 {-# INLINEABLE assetClassValueOf #-}
 
-{- Note [Fused unionWith]
-The previous implementation built an intermediate of type
-@Map CurrencySymbol (Map TokenName (These Integer Integer))@ via a separate
-@unionVal@ helper, then re-walked the result in 'unionWith' to flatten each
-@These@ into a plain @Integer@ by applying @f@. That was three full outer
-passes — @Map.union@, @Map.map unThese@ (yielding inner maps of @These Integer
-Integer@), then @Map.map (Map.map collapse)@ — for a single conceptual merge.
-
-This fused version drops the intermediate stage of inner-@These@ wrapping:
-'fuseInners' walks the outer @Map.union@ result once and, for each currency
-symbol, either applies @f@ in place against a single inner side or merges
-both inner sides via @Map.map collapse (Map.union innerL innerR)@. The
-@Map TokenName (These Integer Integer)@ shape is gone; the outer 'Map.map'
-runs once, not twice. -}
+{- Note [Single-pass unionWith]
+'Map.union' tags each currency symbol with a 'These' recording which side(s)
+hold it. 'fuseInners' consumes that tag in one outer 'Map.map': against an
+implicit @0@ on the absent side, or — when both sides hold the symbol — over
+the inner @Map.union innerL innerR@. The merge therefore touches each level
+once and never materialises a @Map TokenName (These Integer Integer)@. -}
 
 {-| Combine two 'Value' maps with the argument function.
 Assumes the well-definedness of the two maps. -}
@@ -462,11 +454,9 @@ isZero (Value xs) = Map.all (Map.all (\i -> 0 == i)) xs
 {-| Check whether a binary relation holds for value pairs of two 'Value' maps,
   supplying 0 where a key is only present in one of them.
 
-Mirrors 'unionWith' (see Note [Fused unionWith]): a single outer 'Map.union'
-plus one outer 'Map.all'. For currency symbols present in both 'Value's,
-the inner check runs over the inner 'Map.union'. For currency symbols
-present on only one side, the inner check applies the relation against
-@0@ on the missing side. -}
+Shares the structure of 'unionWith' (see Note [Single-pass unionWith]), with
+'Map.all' in place of 'Map.map': the walk short-circuits on the first pair
+that fails @f@, applying the relation against @0@ on whichever side is absent. -}
 checkBinRel :: (Integer -> Integer -> Bool) -> Value -> Value -> Bool
 checkBinRel f (Value mapL) (Value mapR) =
   Map.all checkInners (Map.union mapL mapR)

plutus-tx-plugin/test-ledger-api/Spec/Data/Value.hs

@@ -27,7 +27,7 @@ import PlutusTx.Numeric
 import PlutusTx.Prelude hiding (integerToByteString)
 import PlutusTx.Show (toDigits)
 import PlutusTx.TH (compile)
-import PlutusTx.Test.Run.Code (evalResult, evaluateCompiledCode, evaluationResultMatchesHaskell)
+import PlutusTx.Test.Run.Code (evalResult, evaluateCompiledCode)
 import PlutusTx.Traversable qualified as Tx
 
 import PlutusCore.Builtin qualified as PLC
@@ -319,16 +319,61 @@ test_valueOf =
                   `unsafeApplyCode` liftCodeDef (unTokenName tn)
            in nonBuiltin === builtin
 
-{-| Check that running the compiled fused 'unionWith' on CEK produces the
-same 'Value' as the host-Haskell implementation, for arbitrary pairs of
-'Value's. The combining function must come from 'PlutusTx.Prelude' so
-that Plinth can inline it into the compiled UPLC. -}
+{-| The 'unionWith' @(+)@ under test. Signature matches 'compiledBuiltinUnion' so the property
+can pit them against each other. -}
+compiledUnionWith :: CompiledCode (BI.BuiltinData -> BI.BuiltinData -> BI.BuiltinData)
+compiledUnionWith = plinthc \bd1 bd2 ->
+  Tx.toBuiltinData (unionWith (+) (Tx.unsafeFromBuiltinData bd1) (Tx.unsafeFromBuiltinData bd2))
+
+{-| Independent oracle: the builtin union path. Shares no source with 'compiledUnionWith', so a
+bug in one cannot hide behind the same bug in the other. -}
+compiledBuiltinUnion :: CompiledCode (BI.BuiltinData -> BI.BuiltinData -> BI.BuiltinData)
+compiledBuiltinUnion = plinthc \bd1 bd2 ->
+  B.mkValue (B.unionValue (B.unsafeDataAsValue bd1) (B.unsafeDataAsValue bd2))
+
+-- | Evaluate a compiled union on CEK and decode its result.
+runUnionCode
+  :: CompiledCode (BI.BuiltinData -> BI.BuiltinData -> BI.BuiltinData)
+  -> Value
+  -> Value
+  -> Value
+runUnionCode code value1 value2 =
+  Tx.unsafeFromBuiltinData
+    . BI.dataToBuiltinData
+    . either Haskell.throw id
+    $ errOrRes
+    >>= PLC.readKnownSelf
+  where
+    prog =
+      code
+        `unsafeApplyCode` liftCodeDef (Tx.toBuiltinData value1)
+        `unsafeApplyCode` liftCodeDef (Tx.toBuiltinData value2)
+    (errOrRes, _cost) =
+      PLC.runCekNoEmit PLC.defaultCekParametersForTesting PLC.counting
+        . PLC.runQuote
+        . PLC.unDeBruijnTermWith (Haskell.error "Free variable")
+        . PLC._progTerm
+        $ getPlc prog
+
+-- | 'unionWith' @(+)@ must agree with the builtin union path on CEK.
 test_unionWith :: TestTree
 test_unionWith =
-  testProperty "unionWith on CEK matches host Haskell" \value1 value2 ->
-    let compiled =
-          $$(compile [||\v1 v2 -> unionWith (+) v1 v2||])
-            `unsafeApplyCode` liftCodeDef value1
-            `unsafeApplyCode` liftCodeDef value2
-        expected = unionWith (+) value1 value2
-     in evaluationResultMatchesHaskell compiled (===) expected
+  testProperty "non-builtin unionWith matches builtin unionValue on CEK" \rawValue1 rawValue2 ->
+    let v1 = normalise rawValue1
+        v2 = normalise rawValue2
+        -- Compare semantically: key order and zero-sum entries differ between the paths but
+        -- carry no meaning, so canonicalise before '==='.
+        canon code = normaliseLists . valueToLists $ runUnionCode code v1 v2
+     in canon compiledUnionWith === canon compiledBuiltinUnion
+
+{-| Restrict an arbitrary 'Value' to the well-formed domain 'unsafeDataAsValue' accepts: the
+builtin errors on unsorted keys, zero quantities, or empty token maps. -}
+normaliseLists
+  :: [(CurrencySymbol, [(TokenName, Integer)])] -> [(CurrencySymbol, [(TokenName, Integer)])]
+normaliseLists =
+  Haskell.sortOn fst
+    . Haskell.filter (Haskell.not . Haskell.null . snd)
+    . Haskell.map (Haskell.fmap (Haskell.sortOn fst . Haskell.filter ((Haskell./= 0) . snd)))
+
+normalise :: Value -> Value
+normalise = listsToValue . normaliseLists . valueToLists