Spec.Data.Value.Budget — non-builtin valueOf evidence (NOT FOR MERGE)#7798
Draft
Unisay wants to merge 2 commits into
Draft
Spec.Data.Value.Budget — non-builtin valueOf evidence (NOT FOR MERGE)#7798Unisay wants to merge 2 commits into
Unisay wants to merge 2 commits into
Conversation
Contributor
Contributor
|
2d0ecc7 to
ae21ea2
Compare
152f7a0 to
2e8512e
Compare
ae21ea2 to
0ac70fa
Compare
58a65a7 to
52a8bb6
Compare
0ac70fa to
cd7c252
Compare
52a8bb6 to
ad744d7
Compare
cd7c252 to
8271c9e
Compare
ad744d7 to
804a090
Compare
8271c9e to
613670c
Compare
804a090 to
ea05f7b
Compare
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.
613670c to
b4d1df4
Compare
Adds `Spec.Data.Value.Budget` with the lookup matrix for `valueOf` across S1 / S3 / S8 / S100 value shapes at ada / middle / last / miss positions, plus the standalone `unsafeDataAsValue` baseline per shape. Generated 96 golden files (eval / pir / uplc per bundle, 32 bundles total) capture CPU and Memory cost evidence. Companion to the merge PR for `valueOf` rewrite. This branch is kept separate so the goldens — which only regenerate on upstream plugin or cost-model changes, not on actual regressions — don't bloat the main PR's diff or CI. For IntersectMBO/plutus-private#2242.
ea05f7b to
79a5fde
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Not for merge. The purpose is to compare three lookup paths so that V3 guidance on which to prefer can be backed by concrete numbers rather than estimates:
unsafeDataAsValue+lookupCoin): the new on-chain builtins introduced for Data-backed Values.valueOfpath:plutus-ledger-api'sPlutusLedgerApi.V1.Data.Value.valueOf(after the rewrite in #7797), entered throughunsafeFromBuiltinData.BuiltinDatawalker: a hand-rolledvalueOfRaw :: BuiltinByteString -> BuiltinByteString -> BuiltinData -> Integerthat walks the Data structure directly viaunsafeDataAsMap/unsafeDataAsB/unsafeDataAsI. This is the pre-BuiltinValue baseline that production Plinth code (e.g. Djed) and other compilers (Aiken, Pebble, Scalus) effectively produce.Spec.Data.Value.Budgetruns all three across four shapes (S1 / S3 / S8 / S100) at four lookup positions (ada / middle / last / miss). It also capturesunsafeDataAsValuestandalone per shape, so the decode overhead can be subtracted from the BuiltinValue column. 46 bundles × 3 files = 138 goldens.This branch stacks on top of #7797.
For plutus-private#2242.
Lookup matrix, GHC 9.6, plutus-ledger-api 1.65.0.0
CPU in thousands. Columns:
unsafeDataAsValue+lookupCoin.valueOf=unsafeFromBuiltinData+PlutusLedgerApi.V1.Data.Value.valueOf(the rewrite from #7797).valueOfRaw :: BuiltinByteString -> BuiltinByteString -> BuiltinData -> IntegeroverunsafeDataAsMap/unsafeDataAsB/unsafeDataAsI; the pre-BuiltinValue baseline.Shape legend: S1 = ada only (1 token); S3 = ada plus 2 single-token policies (3 tokens); S8 = ada plus 7 single-token policies (8 tokens); S100 = ada plus 10 policies of 10 tokens each (101 tokens). Lookup position is the row index of the matching
(currency, token)inside the outer/inner maps: ada = first, middle = around the centre, last = final entry, miss = absent key.valueOfNote on the S100 last vs miss asymmetry for typed and raw:
lastwalks the outer fully (11 entries to reachcs10) and then the inner ofcs10(10 entries to reachtn10), whilemissonly walks the outer (11 entries, no inner decoding and walk), solastcosts roughly 21 step-equivalents andmiss11 — a ratio matching the observed CPU split. The BuiltinValue path is position-independent:unsafeDataAsValuedecodes the whole value up front.Standalone
unsafeDataAsValue:Typed
valueOfvs raw walkerPlutusLedgerApi.V1.Data.Valueis Data-backed:Valueis a newtype overData.AssocMap.Map, which is itself a newtype overBuiltinList (BuiltinPair BuiltinData BuiltinData). SounsafeFromBuiltinData :: BuiltinData -> Valuedoes not decode the structure; it coerces through the newtype layers to the underlyingBuiltinList. The Plinth plugin strips this to zero-cost coercions.The typed
valueOfand the raw walker traverse identically once compiled, so the gap between them is small: ~300 K CPU flat on most rows, growing modestly on the larger linear scans (S100 middle / last). The single-percent overhead reflects only the constant newtype-unwrap on the caller boundary, not any per-element work.The typed
valueOfAPI is not appreciably slower than a rawBuiltinDatawalker. Callers who already hold aBuiltinDataand prefer the raw signature can write one inline, but there's no order-of-magnitude reason to exposevalueOfRawpublicly.V3 lookup guidance
Headline: for the values seen on mainnet today (S1–S8, ≤8 assets), the BuiltinValue path is the cheaper choice. It wins at every position by 2×–4× on S1, 1.5×–3× on S3, and stays within 5% of the typed/raw walkers even on S8 ada (the crossover point). Since the vast majority of on-chain values fall in this range, this is the default recommendation.
More detail by size and access pattern:
unsafeDataAsValueoverhead is the whole cost, and it stays small enough that walking (typed or raw) can't beat it.valueOfor a raw walker. The short-circuit beats the linearunsafeDataAsValuedecode on any size, and the gap widens (S100 ada: ~5.9× cheaper than the BuiltinValue path).lookupCoincalls are cheap.The "non-builtin is 2.5–12× slower" claim from #7738 no longer applies for first-position lookups on large values, but the headline for typical-size mainnet values (S1–S8) is now firmly in favour of the BuiltinValue path.