fix(scenarios): encode finite upper bounds as exclusive, drop the closure branch from the time specs

[nau]

Problem

The htlc, two_party_escrow and linear_vesting scenarios each carry a "Note on time semantics" paragraph that requires a validator to handle the closure flag of the txInfoValidRange bounds:

For a finite inclusive upper bound t, upperBound = t; for a finite exclusive upper bound t, upperBound = t − 1. Symmetrically for the lower bound: inclusive t ⇒ lowerBound = t; exclusive t ⇒ lowerBound = t + 1.

The fixtures then use point intervals [t, t], i.e. a finite inclusive upper bound, for every claim and deposit test. The ledger never produces that shape in a PlutusV3 script context (details below). So the inclusive branch is unreachable on-chain, yet every submission has to implement it to pass the fixtures, and CAPE measures it. The three scenarios are the only ones that use set_valid_range.

What the ledger guarantees

CAPE contexts are PlutusV3, and V3 exists only from the Conway era on. In the Conway era the script context of every Plutus version is built by transValidityInterval in eras/conway/impl/src/Cardano/Ledger/Conway/TxInfo.hs (cardano-ledger cardano-ledger-conway-1.22.1.0, the mainnet PV11 pin), lines 793–810:

transValidityInterval _ epochInfo systemStart = \case
  ValidityInterval SNothing SNothing -> pure PV1.always
  ValidityInterval (SJust i) SNothing -> PV1.from <$> transSlotToPOSIXTime i
  ValidityInterval SNothing (SJust i) -> do
    t <- transSlotToPOSIXTime i
    pure $ PV1.Interval (PV1.LowerBound PV1.NegInf True) (PV1.strictUpperBound t)
  ValidityInterval (SJust i) (SJust j) -> do
    t1 <- transSlotToPOSIXTime i
    t2 <- transSlotToPOSIXTime j
    pure $
      PV1.Interval
        (PV1.lowerBound t1)
        (PV1.strictUpperBound t2)

The V1, V2 and V3 EraPlutusTxInfo ... ConwayEra instances all call it (same file, lines 407, 444, 483), and the Dijkstra era reuses it (eras/dijkstra/impl/src/Cardano/Ledger/Dijkstra/TxInfo.hs, lines 251, 310, 349, 445). The helpers are defined in plutus-ledger-api plutus-ledger-api/src/PlutusLedgerApi/V1/Interval.hs (tag 1.63.0.0):

strictUpperBound a = UpperBound (Finite a) False   -- line 285
lowerBound a       = LowerBound (Finite a) True    -- line 297
from s             = Interval (lowerBound s) (UpperBound PosInf True)   -- line 354
always             = Interval (LowerBound NegInf True) (UpperBound PosInf True)  -- line 365

So for every context the ledger hands to a V3 script:

• a finite lower bound is always LowerBound (Finite t) True (inclusive), where t is invalid_before;
• a finite upper bound is always UpperBound (Finite t) False (exclusive), where t is invalid_hereafter (the tx ttl);
• an omitted bound is NegInf / PosInf.

Scope note: the older era-generic translation in eras/alonzo/impl/src/Cardano/Ledger/Alonzo/Plutus/TxInfo.hs (lines 229–243), used by the Alonzo and Babbage eras, translates an upper-bound-only interval with PV1.to, which yields an inclusive upperBound (Interval.hs line 360). That is the one historical case of a finite inclusive upper bound, and it applies to pre-Conway eras only (the dispatch moved from protocol versions to eras in cardano-ledger alonzo 1.14.0.0 / conway 1.20.0.0, which removed hardforkConwayTranslateUpperBoundForPlutusScripts). It cannot occur in a PlutusV3 context. The both-bounds case is strictUpperBound in every era.

Why it matters for a benchmark

• The closure branch is unreachable by construction, not by convention. A validator that reads the closure flag pays for a Constr walk and a conditional on every claim/deposit, and a submission that skips it fails the current fixtures. CAPE exists to compare compilers on realistic script contexts; forcing dead code into every submission skews the numbers it reports.
• "Defensive programming" does not apply here: there is no transaction that can reach the other branch. The ledger, not the transaction author, chooses the closure. Defending against the finiteness of a bound is different: an omitted bound is a legal transaction shape, so those checks and the *_infinite_*_bound tests stay.
• Measured cost of the branch on the current submissions: about 165k CPU / 402 mem per claim or deposit for the submissions that branch on the flag (see the table below). Small in absolute terms, but it is a constant added to every submission for a case that cannot happen.

The change

Semantics preserved. With exclusivity guaranteed, upperBound = t − 1 for Finite t is unconditional and lowerBound = t is the raw finite lower bound. Every fixture with a finite inclusive upper bound t is re-encoded as (Finite (t + 1), False); lower bounds already are (Finite t, True). Under this pairing every converted bound value, and therefore every expected pass/fail outcome, is unchanged, and a submission that still implements the closure branch computes the same value on its exclusive path.

1. lib/Cape/ScriptContextBuilder.hs: set_valid_range now encodes to_time as UpperBound (Finite t) False. from_time stays LowerBound (Finite t) True, omitted bounds stay NegInf / PosInf. The JSON DSL can no longer express a validity interval the ledger would not produce. from_time / to_time map 1:1 onto invalid_before / invalid_hereafter.
2. schemas/cape-tests.schema.json, lib/Cape/Tests.hs: describe from_time as the inclusive lower bound and to_time as the exclusive upper bound.
3. test/Cape/ScriptContextBuilderSpec.hs: expectations follow the builder.
4. scenarios/*/cape-tests.json: every finite to_time bumped by one (table below). Lower bounds and the infinite-bound tests are untouched.
5. scenarios/*/*.md: the three "Note on time semantics" paragraphs state the ledger guarantee instead of the closure conversion table, the [t, t] fixture sentences are rewritten, and the interval notation in the three *_infinite_lower_bound descriptions follows the new encoding. The upper/lower bound choice per path (claim and deposit read the upper bound, refund and unlock read the lower bound) is unchanged. The stale htlc sentence about a follow-up issue now points at Unify validity-range semantics across Linear Vesting and Two-Party Escrow scenarios (post-HTLC follow-up) #171.

Fixture table

Encoded is the POSIXTimeRange the builder produces. Value is the converted bound the spec compares (upperBound = t − 1 for an exclusive Finite t).

Scenario	Fixture(s)	Before: encoded (ledger-possible?)	After: encoded	Value / outcome
htlc	successful_claim baseline, claim_well_before_timeout and every claim check that inherits it	[Finite 50 T, Finite 50 T] (no)	[Finite 50 T, Finite 51 F)	upperBound 50 < 100, unchanged
htlc	claim_just_before_timeout	[99 T, 99 T] (no)	[99 T, 100 F)	upperBound 99 < 100, unchanged (pass)
htlc	claim_at_timeout	[100 T, 100 T] (no)	[100 T, 101 F)	upperBound 100, not < 100, unchanged (error)
htlc	claim_after_timeout	[150 T, 150 T] (no)	[150 T, 151 F)	upperBound 150, unchanged (error)
htlc	claim_infinite_upper_bound	[50 T, PosInf T] (yes)	unchanged	error, stays
htlc	successful_refund baseline, refund_just_after_timeout (101), refund_before_timeout (50), refund_at_timeout (100)	[t T, PosInf T] (yes)	unchanged	lowerBound t, unchanged
htlc	refund_infinite_lower_bound	[NegInf T, 200 T] (no)	[NegInf T, 201 F)	error (NegInf), unchanged
two_party_escrow	successful_deposit baseline and every deposit check that inherits it	[1000 T, 1000 T] (no)	[1000 T, 1001 F)	upperBound 1000 = datum depositTime 1000, unchanged
two_party_escrow	deposit_infinite_upper_bound	[1000 T, PosInf T] (yes)	unchanged	error, stays
two_party_escrow	all refund fixtures (from_time 2801, 3000, 3600, 5000, 2000, 900, 1800)	[t T, PosInf T] (yes)	unchanged	lowerBound t, unchanged
two_party_escrow	refund_infinite_lower_bound	[NegInf T, 3000 T] (no)	[NegInf T, 3001 F)	error (NegInf), unchanged
two_party_escrow	refund_with_no_time_range	always (yes)	unchanged	error, stays
linear_vesting	all unlock fixtures (from_time 11, 101, 50, 91, 25, 200, 5, 10, 100)	[t T, PosInf T] (yes)	unchanged	lowerBound t, unchanged
linear_vesting	partial_unlock_infinite_lower_bound	[NegInf T, 90 T] (no)	[NegInf T, 91 F)	error (NegInf), unchanged
linear_vesting	full_unlock_infinite_lower_bound	[NegInf T, 200 T] (no)	[NegInf T, 201 F)	error (NegInf), unchanged

No fixture changes outcome.

Submissions impact and verification

• Hspec suite: 117 examples, 0 failures.
• cape submission verify on every non-preview submission of the three scenarios (23 directories: htlc 9, two_party_escrow 7, linear_vesting 7): all pass with the same counts as before, 25/25, 47/47 and 29/29. The 12 _preview directories were not re-run (they need measure-preview); they compile the same sources as their production counterparts.
• A/B on the same submissions with matching binaries (main's builder + old fixtures vs this branch's builder + new fixtures), so the delta is the fixture change only:
  • linear_vesting: no CPU/mem change on any evaluation (only the two infinite-lower-bound checks were re-encoded, and they reject before the closure is read).
  • htlc and two_party_escrow, submissions that branch on the closure flag (Plinth 1.45/1.64/1.65, Scalus 0.16/0.17/0.18.2): claim / deposit happy paths +165 208 CPU, +402 mem (the exclusive path does one extra subtractInteger); claim_at_timeout, claim_after_timeout, claim_double_satisfaction +101 208 CPU. Roughly 35 lovelace per claim at mainnet prices.
  • The _asdata / _plain variants go the other way: happy paths −139 174 to −203 174 CPU, and some checks move by larger amounts because the lazy field walk takes a different path.
• Committed metrics.json files are therefore stale by those amounts for htlc and two_party_escrow (aggregates included: cpu_units.sum moves by twice the claim delta for htlc, by the deposit delta for two_party_escrow). CI's cape submission verify --all rewrites metrics.json but does not gate on its content, so this PR passes CI as is. I did not regenerate them here because the _preview variants need the second build and a partial regeneration would leave the set inconsistent; a regeneration of all 35 directories can follow in one pass.

Related

• HTLC: switch claim to upper-bound validity check (production-safe) #170 switched the htlc claim path to the upper bound (production-safe convention).
• Unify validity-range semantics across Linear Vesting and Two-Party Escrow scenarios (post-HTLC follow-up) #171 / fix: unify validity-range semantics across Linear Vesting and Two-Party Escrow #175 unified Linear Vesting and Two-Party Escrow on the same convention. The htlc.md sentence "unification is tracked in a follow-up issue" was stale and now references Unify validity-range semantics across Linear Vesting and Two-Party Escrow scenarios (post-HTLC follow-up) #171.
• This PR keeps the upper/lower bound choice from HTLC: switch claim to upper-bound validity check (production-safe) #170 and fix: unify validity-range semantics across Linear Vesting and Two-Party Escrow #175 and removes only the closure branch.

Out of scope

• The *_infinite_upper_bound / *_infinite_lower_bound tests: an omitted bound is a legal transaction, so the finiteness checks stay.
• Simplifying individual submissions (dropping their closure branch) and regenerating metrics.json: follow-ups, per submission.
• Lower-bound values of existing fixtures (for example refund_at_exact_deadline in two_party_escrow uses from_time = 1800): untouched.