Cardano Updates

The previous commit (642442a85f) regenerated the GHC 9.6 column only.
plutus-ledger-api-plugin-test is also buildable on GHC 9.12 per the
ghc-version-support common stanza, and Hydra runs it there; the
checkBinRel rewrite changes the compiled UPLC enough to move the
budgets in both columns. Same regen, run in nix develop .#ghc912.

For IntersectMBO/plutus-private#2243.

The fusion is a constant-factor change, not the elimination of the These
intermediate it was described as. Map.union still produces a per-key These
and the inner These is still built transiently for shared keys; what the
fusion removes is one of the two outer Map.map passes over the post-union
map, plus the wrap-then-remap of single-side currencies. Adjust the
changelog and drop Note [Single-pass unionWith] accordingly; the merge
structure is plain from the code.

For IntersectMBO/plutus-private#2243.

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.

Drop the internal unionVal and checkPred helpers; inline the merge logic
into unionWith and checkBinRel respectively. The previous chain built a
Map CurrencySymbol (Map TokenName (These Integer Integer)) intermediate
via unionVal, then re-walked it to apply f -- three outer passes for a
single conceptual merge.

The fused unionWith now runs Map.union once and a single outer Map.map,
collapsing the These shape inline per currency-symbol entry. The
Map TokenName (These Integer Integer) stage is gone; the outer Map.map
runs once instead of twice. checkBinRel is refactored along the same
shape with Map.union + Map.all, which gives geq / leq / gt / lt
short-circuit termination on the first failing pair.

Adds Spec.Data.Value.test_unionWith: a QuickCheck property that compiles
unionWith via TH, evaluates on the CEK machine, and compares against the
host-Haskell unionWith for the same inputs. Differential test against
the Plinth compiler: any divergence is a compilation bug, not a
semantics bug.

The Spec.Data.Budget gt / geq budget goldens are regenerated: short-circuit
checkBinRel reduces gt4 / geq4 by ~46% (the worst-case adverse input);
other shapes drop 0.7-3% from removing one outer pass over the These
intermediate. The remaining diff is the cost-model anchor; that
component is unrelated to this change.

Budget evidence (union matrix vs builtin, unsafeDataAsValue baseline)
lives on the companion experimental branch
yura/issue-2243-fused-unionwith-evidence, stacked on the sibling
valueOf-evidence branch.

For IntersectMBO/plutus-private#2243.

The fusion is a constant-factor change, not the elimination of the These
intermediate it was described as. Map.union still produces a per-key These
and the inner These is still built transiently for shared keys; what the
fusion removes is one of the two outer Map.map passes over the post-union
map, plus the wrap-then-remap of single-side currencies. Adjust the
changelog and drop Note [Single-pass unionWith] accordingly; the merge
structure is plain from the code.

For IntersectMBO/plutus-private#2243.

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.

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.

Adds a PIR-readable snapshot and four budget snapshots for the new `valueOf`
implementation, registered alongside the existing golden coverage for
`gt`, `geq`, and `currencySymbolValueOf`.

Scenarios:
- valueOf_hit_first: ada-like first-position lookup, exercises short-circuit on the first outer step.
- valueOf_hit_middle: key at the middle of the outer map.
- valueOf_hit_last: key at the last entry, full outer scan.
- valueOf_miss: absent key, full scan with no inner walk.

These tests catch regressions in `valueOf` compilation and cost that would
otherwise surface only through downstream callers (`currencySymbolValueOf`,
`assetClassValueOf`, `geq`, etc.).

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.

Compares the on-chain builtin union path (unsafeDataAsValue + unionValue +
mkValue) against a hand-rolled sorted-merge over the raw BuiltinData
representation, so V3 guidance on union cost rests on concrete numbers
rather than estimates.

The new module Spec.Data.Value.UnionBudget adds 8 goldenBundle entries:
union_S1,3,8,100 in builtin and raw variants. Both bundle paths take two
BuiltinData-encoded Values, the same value on both sides, mirroring the
conservation-of-value pattern from production validators, produce the
merged BuiltinData, and report the CEK budget. The bundle does not chain
a lookupCoin or valueOf on the result so the measured cost is the union
itself, not a union-then-lookup composite.

The hand-rolled unionValuePositiveRaw is a Plinth translation of
Philip's pvalueUnionFast (Plutarch, slack thread 1776810760.659419).
Sorted-merge with a three-way branch on key comparison; assumes both
inputs sorted by lexicographic key and inner-pair values strictly
positive. Sorted-merge is O(L + R) per level; lookup-and-merge through
AssocMap.union would be O(L x R).

unionValuePositiveRaw is module-internal and not exported from
plutus-ledger-api. The positive-quantity precondition is documented at
the call site, not encoded in the type system. The unionValueNonZero
variant from the slack discussion is left for a follow-up commit; the
production case Philip cares about is tx outputs, which are strictly
positive.

Result matrix, raw vs builtin CPU ratio: S1 5.20x, S3 5.65x, S8 5.83x,
S100 4.47x. Byte-identical output between builtin and raw at every
shape; the raw column closes most of the gap that the typed unionWith
from plutus#7799 opens. Goldens regenerated under both GHC 9.6 and GHC
9.12 (per ghc-version-support cabal stanza). 24 goldens times 2 GHC
versions equals 48 files.

For IntersectMBO/plutus-private#2243.

The previous commit (642442a85f) regenerated the GHC 9.6 column only.
plutus-ledger-api-plugin-test is also buildable on GHC 9.12 per the
ghc-version-support common stanza, and Hydra runs it there; the
checkBinRel rewrite changes the compiled UPLC enough to move the
budgets in both columns. Same regen, run in nix develop .#ghc912.

For IntersectMBO/plutus-private#2243.

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.

Adds a PIR-readable snapshot and four budget snapshots for the new `valueOf`
implementation, registered alongside the existing golden coverage for
`gt`, `geq`, and `currencySymbolValueOf`.

Scenarios:
- valueOf_hit_first: ada-like first-position lookup, exercises short-circuit on the first outer step.
- valueOf_hit_middle: key at the middle of the outer map.
- valueOf_hit_last: key at the last entry, full outer scan.
- valueOf_miss: absent key, full scan with no inner walk.

These tests catch regressions in `valueOf` compilation and cost that would
otherwise surface only through downstream callers (`currencySymbolValueOf`,
`assetClassValueOf`, `geq`, etc.).

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.

Adds semantic definitions of values and purity, based on the current UPLC reduction semantics. Also changes Reduction.lagda.md semantics to be closer to the pdf spec, in the sense that it is only defined for closed terms.

Semantic versions of Value and Pure are needed for proving certain translation relations sound. Proving that Pure (syntactic) implies pure (semantic) will be next.