I wasn't aware of this feature being implemented as part of Conway. You're completely right, if this is supported now this needs to be part of the spec. This should be fairly easy to do, just have to adjust a couple of types and functions. I don't think this will touch any proofs.

@lehins can you confirm that this is an intended feature? If so, this should have been communicated to us properly.

@WhatisRT Yes, it is the CIP-69, which was indeed implemented for Conway era. I am really surprised you did not know about it. It was a big deal we even had to get an explicit approval from Charles to postpone the Chang hard fork in order to implement it.

I only remember it coming up occasionally, but I wasn't in any meeting where a decision was made and it was never raised as something that we (formal methods) need to implement.

I'll give this a high priority for the spec release, should be fixed in a few weeks at the latest.

I was going to write an implementation plan for this, but then I realized that there is actually nothing to do for the actual semantics, because we have a bug in our current Alonzo implementation. The spec actually allows the case for the datum being empty already (the Alonzo spec does forbid this explicitly though).

So all that needs to be done here is to document and expose this. Specifically, this line

∙  inputHashes ⊆ txdatsHashes

compares two ℙ DataHash, while in the original Alonzo spec it would have been ℙ (Maybe DataHash) (even though that spec is untyped). Here, a nothing gets just thrown out, while in the original spec the rhs could never contain a nothing so the lhs was forbidden from containing one either.

@williamdemeo can you add a small section to Ledger.Utxow explaining that & make sure that the figure showing UTXOW-inductive and getInputHashes are visible in the Conway spec? There's a NoConway environment that currently blocks the rule from being shown. This section should also reference CIP-69. I don't remember the status of the highlighting tool right now, but ideally the line inputHashes ⊆ txdatsHashes should be highlighted.