Skip to content

Commit cd7c252

Browse files
committed
Optimal non-builtin valueOf in plutus-ledger-api Data.Value
Rewrites `PlutusLedgerApi.V1.Data.Value.valueOf` so the non-builtin lookup path walks the underlying `BuiltinList` directly via `unsafeDataAsMap` / `unsafeDataAsB` / `unsafeDataAsI`, compares keys with `equalsByteString`, and short-circuits on the first match. No `Maybe` is materialised: the "absent" answer is `0`, returned in-place by the `nilCase` of each traversal. Avoids `withCurrencySymbol`'s continuation + `Map.lookup`'s `Maybe`-wrapping, and bypasses the `ToData k`/`UnsafeFromData a` dictionary work that `AssocMap.lookup` does per element. Semantics preserved. Adds `Spec.Data.Value.test_valueOf`: a QuickCheck property that compiles `valueOf` via TH, evaluates it on the CEK machine, and compares the result against the host-Haskell `valueOf` for the same inputs. Differential test against the Plinth compiler — any divergence is a compilation bug, not a semantics bug. Budget evidence (lookup matrix, `unsafeDataAsValue` baseline) lives on the companion experimental branch `yura/issue-2242-valueof-evidence`, kept out of this PR to avoid carrying ~96 golden files that would only ever regenerate on upstream plugin/cost-model changes. For IntersectMBO/plutus-private#2242.
1 parent 22a716e commit cd7c252

4 files changed

Lines changed: 92 additions & 5 deletions

File tree

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
### Changed
2+
3+
- `PlutusLedgerApi.V1.Data.Value.valueOf` rewritten to walk the underlying `BuiltinList` directly via `unsafeDataAsMap` / `unsafeDataAsB` / `unsafeDataAsI` and short-circuit on the first match. The previous implementation went through `Map.lookup`, which materialised a `Maybe` only to deconstruct it immediately, and paid `ToData k` / `UnsafeFromData a` dictionary work per element. Semantics are unchanged.

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

Lines changed: 12 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -336,11 +336,18 @@ instance MeetSemiLattice Value where
336336
{-| Get the quantity of the given currency in the 'Value'.
337337
Assumes that the underlying map doesn't contain duplicate keys. -}
338338
valueOf :: Value -> CurrencySymbol -> TokenName -> Integer
339-
valueOf value cur tn =
340-
withCurrencySymbol cur value 0 \tokens ->
341-
case Map.lookup tn tokens of
342-
Nothing -> 0
343-
Just v -> v
339+
valueOf (Value mp) (CurrencySymbol curBs) (TokenName tnBs) =
340+
goOuter (Map.toBuiltinList mp)
341+
where
342+
goOuter = B.caseList' 0 \hd ->
343+
if B.equalsByteString curBs (BI.unsafeDataAsB (BI.fst hd))
344+
then \_ -> goInner (BI.unsafeDataAsMap (BI.snd hd))
345+
else goOuter
346+
347+
goInner = B.caseList' 0 \hd ->
348+
if B.equalsByteString tnBs (BI.unsafeDataAsB (BI.fst hd))
349+
then \_ -> BI.unsafeDataAsI (BI.snd hd)
350+
else goInner
344351
{-# INLINEABLE valueOf #-}
345352

346353
{-| Apply a continuation function to the token quantities of the given currency

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,7 @@ tests =
2727
, Spec.Data.Budget.tests
2828
, Spec.Data.ScriptContext.tests
2929
, Spec.Data.Value.test_EqValue
30+
, Spec.Data.Value.test_valueOf
3031
, Spec.Data.MintValue.V3.tests
3132
, Spec.Envelope.tests
3233
, Spec.ReturnUnit.V1.tests

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

Lines changed: 76 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
{-# LANGUAGE BlockArguments #-}
12
{-# LANGUAGE DataKinds #-}
23
{-# LANGUAGE OverloadedStrings #-}
34
{-# LANGUAGE TemplateHaskell #-}
@@ -13,8 +14,11 @@ import Prelude qualified as Haskell
1314
import PlutusLedgerApi.V1.Data.Value
1415

1516
import PlutusTx.Base
17+
import PlutusTx.Builtins qualified as B
18+
import PlutusTx.Builtins.Internal qualified as BI
1619
import PlutusTx.Code (CompiledCode, getPlc, unsafeApplyCode)
1720
import PlutusTx.Data.AssocMap qualified as AssocMap
21+
import PlutusTx.IsData qualified as Tx
1822
import PlutusTx.Lift
1923
import PlutusTx.List qualified as List
2024
import PlutusTx.Maybe
@@ -31,12 +35,16 @@ import UntypedPlutusCore qualified as PLC
3135
import UntypedPlutusCore.Evaluation.Machine.Cek qualified as PLC
3236

3337
import Control.Exception qualified as Haskell
38+
import Data.ByteString qualified as BS
3439
import Data.Functor qualified as Haskell
3540
import Data.List qualified as Haskell
3641
import Data.Map qualified as Map
42+
import PlutusLedgerApi.Test.V1.Data.Value qualified as ListToValue
3743
import Prettyprinter qualified as Pretty
44+
import Test.QuickCheck (Arbitrary (arbitrary), forAll, (===))
3845
import Test.Tasty
3946
import Test.Tasty.Extras
47+
import Test.Tasty.QuickCheck (testProperty)
4048

4149
scalingFactor :: Integer
4250
scalingFactor = 4
@@ -258,3 +266,71 @@ test_EqValue =
258266
$ [ test_EqCurrencyList "Short" currencyListOptions
259267
, test_EqCurrencyList "Long" currencyLongListOptions
260268
]
269+
270+
-- | Compiled non-builtin 'valueOf', evaluated on CEK by the property test.
271+
compiledValueOf :: CompiledCode (Value -> CurrencySymbol -> TokenName -> Integer)
272+
compiledValueOf = $$(compile [||valueOf||])
273+
274+
{-| Compiled builtin lookup: @\\bd cs tn -> lookupCoin cs tn (unsafeDataAsValue bd)@.
275+
Used as the independent oracle in the differential property test for 'valueOf'. -}
276+
compiledBuiltinLookup
277+
:: CompiledCode (BI.BuiltinData -> BI.BuiltinByteString -> BI.BuiltinByteString -> Integer)
278+
compiledBuiltinLookup =
279+
$$(compile [||\bd c t -> B.lookupCoin c t (B.unsafeDataAsValue bd)||])
280+
281+
-- | Run a compiled program that produces an 'Integer' on the CEK machine.
282+
runIntegerOnCek :: CompiledCode Integer -> Integer
283+
runIntegerOnCek prog =
284+
let (errOrRes, _) =
285+
PLC.runCekNoEmit PLC.defaultCekParametersForTesting PLC.counting
286+
. PLC.runQuote
287+
. PLC.unDeBruijnTermWith (Haskell.error "Free variable")
288+
. PLC._progTerm
289+
$ getPlc prog
290+
in either Haskell.throw id $ errOrRes >>= PLC.readKnownSelf
291+
292+
{-| Check that the non-builtin 'valueOf' agrees with the builtin lookup path
293+
('unsafeDataAsValue' + 'lookupCoin') when both are evaluated on the CEK machine.
294+
The two paths share no source code, so any disagreement is a bug in one of them.
295+
296+
The builtin path enforces ledger-level well-formedness that the non-builtin
297+
path does not: 'unsafeDataAsValue' rejects values whose currency symbols or
298+
token names are not sorted, contain duplicates, or where any inner token map is
299+
empty, or any quantity is zero. The arbitrary 'Value' generator may produce any
300+
of these, so each generated value is normalised (zero-quantity tokens dropped,
301+
empty currencies dropped, both maps sorted) before comparison; the equality
302+
only holds for well-formed 'Value's. -}
303+
test_valueOf :: TestTree
304+
test_valueOf =
305+
testProperty "non-builtin valueOf matches builtin lookupCoin on CEK" \rawValue ->
306+
let value =
307+
ListToValue.listsToValue
308+
. Haskell.sortOn fst
309+
. Haskell.filter (Haskell.not . Haskell.null . snd)
310+
. Haskell.map
311+
( Haskell.fmap
312+
( Haskell.sortOn fst
313+
. Haskell.filter ((Haskell./= 0) . snd)
314+
)
315+
)
316+
$ ListToValue.valueToLists rawValue
317+
genBytes = Haskell.fmap BS.pack arbitrary
318+
genKeyPair =
319+
Haskell.liftA2
320+
(\bs1 bs2 -> (currencySymbol bs1, tokenName bs2))
321+
genBytes
322+
genBytes
323+
in forAll genKeyPair \(cs, tn) ->
324+
let nonBuiltin =
325+
runIntegerOnCek
326+
$ compiledValueOf
327+
`unsafeApplyCode` liftCodeDef value
328+
`unsafeApplyCode` liftCodeDef cs
329+
`unsafeApplyCode` liftCodeDef tn
330+
builtin =
331+
runIntegerOnCek
332+
$ compiledBuiltinLookup
333+
`unsafeApplyCode` liftCodeDef (Tx.toBuiltinData value)
334+
`unsafeApplyCode` liftCodeDef (unCurrencySymbol cs)
335+
`unsafeApplyCode` liftCodeDef (unTokenName tn)
336+
in nonBuiltin === builtin

0 commit comments

Comments
 (0)