Cardano Updates

Co-authored-by: Joseph Fajen <[email protected]>

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

Update PlutusIR rewrite rules to handle the new 7-argument
ChooseData builtin. Ensures optimization passes correctly
transform array-related code patterns.

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.

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.

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.

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.

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.

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.

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 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.