Cardano Updates

Kenneth requested more data points above the diagonal for a better
average of the constant-cost region.

Changes:
- Increased from 3 to 20 above-diagonal samples
- Added variety in container/contained size ratios:
  * Small containers (4-16 entries) with larger contained
  * Medium containers (25-100 entries) with larger contained
  * Large containers (150-1024 entries) with much larger contained
- Total benchmark points: ~570 (550 below + 20 above diagonal)

Co-authored-by: Ana Pantilie <[email protected]>

Co-authored-by: Ana Pantilie <[email protected]>

Co-authored-by: Ana Pantilie <[email protected]>

Co-authored-by: Ana Pantilie <[email protected]>

Co-authored-by: Yura <[email protected]>

Co-authored-by: Yura <[email protected]>

Two different "diagonal" concepts were confused:
1. Value structure diagonal (numPolicies vs tokensPerPolicy)
2. Costing diagonal (container totalSize vs contained totalSize)

The previous `aboveDiagonalCombos` tested #1 but the cost model needs #2.

Changes:
- Remove misleading `aboveDiagonalCombos` variable
- Add true above-diagonal samples where contained size > container size
- Update comments to clarify both diagonal concepts
- Generate 3 independent (container, contained) pairs for the constant-cost region

Closes #7525

Update Agda conformance test expected failures to include newly added round-trip and normalization tests. The Agda metatheory has not yet implemented these builtins.

The max-key-len constraint is enforced at the Value type level, not by the valueData builtin. Tests in constant/value/max-key-length-* already cover this constraint.