Agda metatheory has no notion of builtin semantics variants (protocol-era-dependent builtin behavior) -- consByteString is the current concrete case

[jmchapman]

consByteString has two genuinely different behaviors in the real Haskell implementation, dispatched by builtin semantics variant: V1 (truncating, via fromIntegral) and V2 (strict, errors on out-of-range input). Per plutus-ledger-api/src/PlutusLedgerApi/{V1,V2}/EvaluationContext.hs, DefaultFunSemanticsVariantA/B (both -> V1) correspond to real, permanent Cardano protocol eras -- pre-Chang and post-Conway-pre-Van-Rossem -- not abstract/deprecated placeholders.

The Agda metatheory (Builtin.lagda.md:626-629) has no concept of semantics variants anywhere -- no BuiltinSemanticsVariant-equivalent type, no variant parameter on State/step/stepper/BUILTIN. It has exactly one live binding for consByteString, currently V2, applied unconditionally regardless of which era a term targets. This was previously touched in #6055, but that issue's closing discussion only verified V2-Agda-vs-V2-Haskell consistency -- it didn't address whether Agda can still evaluate a term meant for the still-permanently-relevant V1 eras.

The core problem, independent of intended scope: there's no way to tell, from Agda's implementation, that it's only modeling one era, and no mechanism to reject a term meant for a different one -- it silently applies V2 semantics to everything.

A working reference exists: the external Lean 4 PlutusCoreBlaster reimplementation does this correctly -- consByteString takes an explicit semanticsVariant parameter and dispatches exactly like Haskell (PlutusCore/UPLC/BuiltinFunctions/ByteString.lean), threaded through from the ledger version tag used in its test harness.

Two reasonable paths forward -- this issue is meant to surface the scoping question, not presume the answer:

1. Scope Agda explicitly to the latest era, and make that scope explicit and safe -- document it clearly and, ideally, reject/error on a term specifying an era Agda doesn't model, rather than silently misapplying the wrong semantics.
2. Extend Agda to genuinely support multiple variants, enabling full genesis-to-present conformance testing against a formally-verified reference -- threading a variant parameter through State/step/stepper/BUILTIN and updating every caller, following the same shape as Lean's existing implementation.

[kwxm]

@ana-pantilie Do you have a view on this?

[ana-pantilie]

It's a known issue that we don't support multiple semantic versions in the metatheory. However, the biggest issue the metatheory has is that it postulates a high amount of builtin functions and builtin types. We discussed to first implement the most recent version for every "non-crypto" builtin, and once we have a way to conformance test multiple semantic versions we'll adapt the metatheory to support all versions.