Array data constructor and builtins #7485
Draft
+20,536
−12,554
Conversation
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
Add Array as a new Data constructor using Vector for efficient array representation. This enables compact encoding of homogeneous data sequences and improves performance for array-heavy smart contracts. The Array constructor uses CBOR tag 128 for encoding, following the CBOR specification for alternative array representations. This provides better memory efficiency compared to linked lists for large sequential data structures.
Implement ArrayData (tag 101) and UnArrayData (tag 102) builtins for constructing and deconstructing Array data. These builtins enable efficient conversion between Vector and Data representation. Update ChooseData to handle the new Array constructor by adding a seventh branch parameter, maintaining backwards compatibility with proper error handling for non-Array data in UnArrayData.
Add costing functions and models for ArrayData, UnArrayData, and updated ChooseData (now 7-argument). Cost models derived from benchmark data provide accurate execution cost estimates for array operations. Update all three cost model variants (A, B, C) with identical parameters for consistency across evaluation contexts.
Add PlutusTx compiler support for array builtins and update IsData instances to handle Array constructor. This enables Haskell smart contract code to use array data representations with automatic compilation to Plutus Core. Update AssocMap to work with the new 7-argument ChooseData.
Update evaluation contexts across all Plutus versions (V1, V2, V3) to include the new array builtins. This makes ArrayData and UnArrayData available to on-chain validators and scripts. Add plutus-core dependency to analyse-script-events for array support in script analysis tooling.
Extend Agda metatheory with Array constructor and array builtins. Update CEK machine semantics, builtin signatures, and all generated Haskell code from Agda to maintain formal correspondence between specification and implementation. This ensures the array feature is fully formalized and verified in the Plutus metatheory.
Add comprehensive conformance tests for ArrayData, UnArrayData, and updated ChooseData builtin. Tests cover success cases, error handling, and budget validation to ensure consistent behavior across Plutus implementations. Tests include array construction, deconstruction, and proper error messages when UnArrayData receives non-Array data.
Regenerate all golden test files affected by the array feature: - Budget changes from ChooseData parameter addition - UPLC and PIR output with array constructors - Type synthesis tests for new builtins - Evaluation trace changes from updated cost models Golden files updated include test suites, benchmarks, examples, and stdlib tests across plutus-core, plutus-tx-plugin, plutus-benchmark, and cardano-constitution packages.
Update PlutusIR rewrite rules to handle the new 7-argument ChooseData builtin. Ensures optimization passes correctly transform array-related code patterns.
Contributor
Execution Budget Golden Diffoutputplutus-benchmark/cardano-loans/test/9.6/main.golden.eval
plutus-benchmark/linear-vesting/test/9.6/main.golden.eval
plutus-benchmark/lists/test/Sum/9.6/left-fold-data.golden.eval
plutus-benchmark/lists/test/Sum/9.6/right-fold-data.golden.eval
plutus-benchmark/script-contexts/test/V1/9.6/checkScriptContextEqualityData-20.golden.eval
plutus-benchmark/script-contexts/test/V1/Data/9.6/checkScriptContextEqualityData-20.golden.eval
plutus-benchmark/script-contexts/test/V2/9.6/checkScriptContextEqualityData-20.golden.eval
plutus-benchmark/script-contexts/test/V2/9.6/dataFwdStakeTrick.golden.eval
plutus-benchmark/script-contexts/test/V2/9.6/dataFwdStakeTrickManual.golden.eval
plutus-benchmark/script-contexts/test/V2/Data/9.6/checkScriptContextEqualityData-20.golden.eval
plutus-benchmark/script-contexts/test/V3/9.6/checkScriptContextEqualityData-20.golden.eval
plutus-benchmark/script-contexts/test/V3/Data/9.6/checkScriptContextEqualityData-20.golden.eval
plutus-benchmark/script-contexts/test/V3/Data/9.6/purposeIsWellFormed-4.golden.eval
plutus-ledger-api/test-plugin/Spec/Data/Budget/9.6/currencySymbolValueOf.golden.eval
plutus-ledger-api/test-plugin/Spec/Data/Budget/9.6/geq1.golden.eval
plutus-ledger-api/test-plugin/Spec/Data/Budget/9.6/geq2.golden.eval
plutus-ledger-api/test-plugin/Spec/Data/Budget/9.6/geq3.golden.eval
plutus-ledger-api/test-plugin/Spec/Data/Budget/9.6/geq4.golden.eval
plutus-ledger-api/test-plugin/Spec/Data/Budget/9.6/geq5.golden.eval
plutus-ledger-api/test-plugin/Spec/Data/Budget/9.6/gt1.golden.eval
plutus-ledger-api/test-plugin/Spec/Data/Budget/9.6/gt2.golden.eval
plutus-ledger-api/test-plugin/Spec/Data/Budget/9.6/gt3.golden.eval
plutus-ledger-api/test-plugin/Spec/Data/Budget/9.6/gt4.golden.eval
plutus-ledger-api/test-plugin/Spec/Data/Budget/9.6/gt5.golden.eval
plutus-tx-plugin/test/Budget/9.6/map1.golden.eval
plutus-tx-plugin/test/Budget/9.6/map2.golden.eval
plutus-tx-plugin/test/Budget/9.6/map3.golden.eval
plutus-tx-plugin/test/CallTrace/9.6/successfullEvaluationYieldsNoTraceLog.golden.eval
plutus-tx-plugin/test/DataList/Budget/9.6/elem.golden.eval
This comment will get updated when changes are made. |
Unisay
changed the title
Update LaTeX specification documents to document the new Array constructor: builtins1.tex: - Add Array (Vector Data) to Data type definition - Update set-theoretic denotation with Array component - Add injection (inj_A) and projection (proj_A) functions - Add is_A to boolean test functions - Add (Array ...) to concrete syntax - Update chooseData from 6 to 7 arguments with t_A branch - Add arrayData and unArrayData builtins to table data-cbor.tex: - Add Array to Data type definition - Add encoder: Array uses CBOR tag 128 + indefinite list - Add decoder case for tag 128
Unisay
force-pushed
the
yura/issue-1666-data-array-core
branch
from
80756e1 to
470618e
Compare
Update ChooseData benchmark to account for the new Array data constructor. The benchmark now uses mkApp7 with six result arguments instead of mkApp5 with five, and includes comments clarifying which argument corresponds to which Data constructor case.
Update CPU cost parameters for chooseData, equalsData, and serialiseData builtins to reflect accurate benchmarking with the new Array data constructor. Notable changes include chooseData cost reduction (now handles 7 cases efficiently) and adjusted slopes for data comparison operations.
Update all golden test files to reflect the new budget calculations from the updated cost model parameters. Changes span conformance tests, benchmark tests, and plugin tests across V1, V2, and V3 script contexts.
Reorder Array constructor from position 4 to position 6 in the Data type definition and all pattern matches. This makes Array the final constructor, matching its role as an extension to the original 5-constructor Data type (Constr, Map, List, I, B).
Create new Batch 7 section documenting the unreleased Array constructor for the data type and its associated arrayData/unArrayData functions. Move these functions from Batch 1 to Batch 7 to accurately reflect that they will be released in a future protocol version along with the Array constructor itself. Add explanatory note in Batch 1 clarifying Array's future availability.
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.
Context
Approach
This PR implements a new
Arrayconstructor for theDatatype usingVectorfor efficient array representation. The implementation follows the established pattern for data constructors and builtins in Plutus Core.Key Technical Decisions:
CBOR Encoding: Uses CBOR tag 128 for Array encoding, following CBOR specification for alternative array representations. This provides a compact encoding distinct from the existing List constructor.
ChooseData Update: Extended
ChooseDatafrom 6 to 7 arguments to handle the new Array branch. This is a breaking change for existing code using ChooseData, but maintains backwards compatibility at the protocol level through proper versioning.Cost Models: Derived new costing functions from benchmark data for ArrayData, UnArrayData, and the updated ChooseData. All three cost model variants (A, B, C) are updated identically to maintain consistency across evaluation contexts.
Formal Verification: Extended Agda metatheory to include Array constructor and builtins, ensuring the implementation maintains formal correspondence between specification and execution semantics.
The implementation touches all layers of the Plutus stack: core data representation, builtin machinery, compiler support, ledger API integration, and formal verification.
Changes
Specification
doc/plutus-core-spec/cardano/builtins1.texwith Array type definition, injections/projections, concrete syntax, updated chooseData, and new builtinsdoc/plutus-core-spec/data-cbor.texwith CBOR encoding/decoding specification for Array (tag 128)Core Data Type
Array (Vector Data)constructor toPlutusCore.DataData.Vector.Orphansfor required instancesBuiltins
ArrayData(tag 101) builtin for constructing Array from VectorUnArrayData(tag 102) builtin for deconstructing Array to VectorChooseDatato 7-argument form with Array branchCost Models
BuiltinCostModel,CostingFun, andExBudgetingDefaultsPlutusTx Support
IsDatainstances to handle Array constructorAssocMapto work with 7-argument ChooseDataLedger API
Metatheory
PlutusIR
Testing
Breaking Changes
ChooseData Signature Change: The
ChooseDatabuiltin now requires 7 arguments instead of 6 (added Array branch). Existing scripts using ChooseData will need to be recompiled, but this change is isolated to the builtin signature and does not affect on-chain compatibility due to proper versioning.Test Plan