It's probably a good idea to document globalScripts and globalData above where they're first introduced, since they're central to the new Dijkstra semantics. Could you add something like the following above this code block?

• globalScripts : ℙ Script denotes the batch-wide script pool, available for resolving script hashes (witness scripts + reference scripts reachable via reference inputs, possibly including outputs created earlier in the batch).
• globalData : DataHash ⇀ Datum denotes the batch-wide datum pool, available for resolving datum hashes (witness datums + datums reachable via reference inputs and/or other transactions in the batch).

Of course you should revise the prose if you have a better or different understanding of the roles played by these objects.

I'll leave this to the corresponding issue.

I think we should put something other than ∅ here for now, since otherwise the neededDataHashes ⊆ dom (Γ .globalData) fails for all nonempty neededDataHashes.

The suggestion above (DatumMapOf tx) should work if you put the following in Dijkstra/Specification/Transaction.lagda.md:

  record HasDatumMap {a} (A : Type a) : Type a where
    field DatumMapOf : A → DataHash ⇀ Datum
  open HasDatumMap ⦃...⦄ public

  instance
    HasDatumMap-TxWitnesses : HasDatumMap (TxWitnesses txLevel)
    HasDatumMap-TxWitnesses .DatumMapOf = TxWitnesses.txData

    HasDatumMap-Tx : HasDatumMap (Tx txLevel)
    HasDatumMap-Tx .DatumMapOf = DatumMapOf ∘ TxWitnessesOf

Similarly, we should probably put a non-empty placeholder in globalScripts. (Maybe something like witness scripts ∪ ref-input scripts?)

I suggest we leave this to the corresponding issue.

I think we should document asap the important semantic choice of using utxo₀ in both UTXOW and SUBUTXOW to compute scripts/data needed from spending inputs:

range (utxo₀ ∣ txIns)

which encodes the policy spending inputs are always resolved from the initial snapshot (utxo₀). (The "mempool-safety" / "no subtransaction spends newly created outputs" semantics.)

For now maybe just add one sentence above the relevant code blocks, something like,

"In SUBUTXOW, needed scripts/data for txIns are looked up in utxo₀ rather than the current s.utxo since subtransactions cannot spend outputs created earlier in the batch."

By the way, in my PR, I'll rename utxoSpend₀ → utxo₀ (pre-batch snapshot used for spending-input inspection + realizedInputs) and keep utxoRefView (ref-input lookup view, potentially evolving to include earlier-prefix outputs), and I'll add something like the following above where they're introduced:

"utxo₀{.AgdaField} is the pre-batch snapshot used for spending-input inspection and TxInfo.realizedInputs{.AgdaField}; utxoRefView{.AgdaField} is the reference-lookup view (which may include earlier-prefix outputs)."