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

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

Start with Builtin.lagda.md:626-629 and inspect how State, step, stepper, and BUILTIN are defined and used. Compare the variant parameter flow in PlutusCore/UPLC/BuiltinFunctions/ByteString.lean with the Haskell V1 and V2 EvaluationContext files, then establish whether the accepted result is explicit latest-era scoping or support for multiple variants, with tests demonstrating that unsupported or selected-era behavior is not silently misapplied.

Written by the indexing model from the issue text.