[Dijkstra] UTXOW rule

[carlostome]

Description

Stacked PR (Please review PR #1014 before this one!)

The branch of this PR should be rebased on master once PR #1015 is merged.

This PR adapts and adds those preconditions present in Conway to the UTXOW rule.

Still TBD: #1024 #1025

Checklist

• Commit sequence broadly makes sense and commits have useful messages
• Any semantic changes to the specifications are documented in CHANGELOG.md
• Code is formatted according to CONTRIBUTING.md
• Self-reviewed the diff

[williamdemeo]

This looks great. I made some comments/change requests, but nothing too major. Otherwise, nice work, Carlos!

[williamdemeo]

Suggested change

	globalData = ∅ -- TODO
	globalData = DatumMapOf tx -- TODO

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?)

[carlostome]

I suggest we leave this to the corresponding issue.

[williamdemeo]

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)."

[williamdemeo]

This block is essentially a repeat of the let..in block of SUBUTXOW. I wonder if it's worth factoring out this block and placing it in a parametrized module, e.g.,

module UTxOWContext
  (ℓ : TxLevel)
  (Γ : UTxOEnv)
  (s : UTxOState)
  (tx : Tx ℓ)
  where

  ...(stuff inside your let..in block)...

so that, in the definitions of the rules, we can just do:

let open UTxOWContext TxLevelSub Γ s stx in

and

let open UTxOWContext TxLevelTop Γ s tx in

[carlostome]

I think there is a better opportunity here, that is, make the rule level-parametric. Since this is a matter of refactoring but doesn't change the intention I suggest we leave this as work for the near future.

[williamdemeo]

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.

[carlostome]

I'll leave this to the corresponding issue.

[williamdemeo]

This looks good. Let's get this merged once conflicts are resolved.