[Dijkstra] TxBody replace txRequiredGuards

[williamdemeo]

Description

This closes issue #1000.

This PR addresses two issues

1. CIP-0112 upgrades required signers to a set of credentials (key or script), but we currently use ℙ KeyHash, which cannot represent required guard scripts.

2. We should intentionally model signers and guards as distinct concepts: signers feed phase-1/native scripts, guards are the new Dijkstra (CIP-0112/0118) execution requirements.

by doing the following:

• Introduce/rename TxBody field (previously called txRequiredGuards) present at both top- and sub-levels:

  • txGuards : … Credential … (container tbd: List, OSet, etc)

• Replace all uses of txRequiredGuards in Dijkstra with the new credential container.

• Keep TxInfo.vkKey as a key-only view derived from txGuards (CIP-0112's required_observers).

  • Remove reqSignerHashes from TxBody.
  • Add reqSignerHashes : ℙ KeyHash helper/definition (projection from txGuards).
  • Replace uses of TxBody.reqSignerHashes with that helper.
  • Keep TxInfo.vkKey as a key-only view derived from txGuards. This avoids having two independent TxBody fields representing overlapping requirements. (See Carlos' comment.)

  Reason. Even in Dijkstra, we still need the old "required signers / signatories" concept for:

  • phase-1 key witness checking (signatures in vKeySigs)
  • native scripts / timelocks (validP1Script : ℙ KeyHash → ... → P1Script → Type still needs a ℙ KeyHash)
  • and (for now) the TxInfo.vkKey : ℙ KeyHash field aligns with/needs a "key hashes that count as signatories"

---

Copilot-generated Description (manually reviewed and revised)

This pull request introduces several updates to the Dijkstra specification, focusing on transaction guard handling and the transaction info structure. The changes standardize how required signers and guards are represented and accessed, and update the terminology and field names for clarity and alignment with recent proposals. Additionally, some minor documentation and formatting improvements are included.

Transaction guard and signer handling:

• Renamed the TxBody.txRequiredGuards field to TxBody.txGuards and changed its type to ℙ Credential, representing credentials (either key or script) required by the transaction.
• Changed TxBody.reqSignerHashes from an (independent) field to a (dependent) function, which derives key hashes from the TxBody.txGuards field.
• Updated the TxInfo record and the txInfo function to use the new txGuards field and reqSignerHashes function, ensuring that both native/phase-1/timelock signers and CIP-0112/0118 guards are represented.

Documentation and specification updates:

• Updated the changelog to reflect the changes from txRequiredGuards to txGuards and the addition of reqSignerHashes.
• Added and adjusted code block delimiters and comments for Agda code sections in specification files to improve readability and documentation. [1] [2] [3] [4] [5]

Minor formatting fixes:

• Removed an unnecessary blank line in an import section for consistency.

---

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

[Copilot]

Pull request overview

This PR refactors the Dijkstra transaction specification to properly separate the concepts of "signers" and "guards" in accordance with CIP-0112/0118. The key change is renaming txRequiredGuards to txGuards and upgrading its type from ℙ KeyHash to ℙ Credential to support both key and script credentials. A new reqSignerHashes field is added to maintain backward compatibility for phase-1/native script validation.

• Renamed TxBody.txRequiredGuards to TxBody.txGuards with upgraded type ℙ Credential
• Added TxBody.reqSignerHashes : ℙ KeyHash for phase-1 script signers
• Updated TxInfo record and txInfo functions to map the new fields correctly

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated no comments.

File	Description
src/Ledger/Dijkstra/Specification/Transaction.lagda.md	Updates TxBody record with renamed txGuards field and new reqSignerHashes field
src/Ledger/Dijkstra/Specification/Script/Validation.lagda.md	Updates TxInfo record to include both vkKey and txGuards fields, and updates txInfo function implementations to map from the new TxBody fields
CHANGELOG.md	Documents the semantic changes to TxBody field names and additions

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[carlostome]

I'm not sure this is the right way to go. Decoupling reqSignerHashes from txGuards has a couple of drawbacks:

• The CDDL specification in CIP-0112, states that in TxBody , required_signers field is replaced by required_observers (or guards in nested transactions nomenclature).
• There would be semantic duplication between phase-1 scripts contained in txRequiredGuards and those contained in reqSignerHashes.

[williamdemeo]

I'm not sure this is the right way to go. Decoupling reqSignerHashes from txGuards has a couple of drawbacks:

• The CDDL specification in CIP-0112, states that in TxBody , required_signers field is replaced by required_observers (or guards in nested transactions nomenclature).
• There would be semantic duplication between phase-1 scripts contained in txRequiredGuards and those contained in reqSignerHashes.

Nice observation. You're exactly right on both points. If we kept both TxBody.txGuards : ℙ Credential and TxBody.reqSignerHashes : ℙ KeyHash, then we would have two independent sources of "required signer-ish requirements" which could drift apart... not good.

As simple fix is to

• keep txGuards : ℙ Credential

• make reqSignerHashes a derived view (not a TxBody field) or "projection" (inside the TxBody record type, though I suppose it could be defined outside instead):

  reqSignerHashes : ℙ KeyHash
  reqSignerHashes = mapPartial isKeyHashObj txGuards

As for TxInfo.vkKey and TxInfo.txGuards, CIP-0112 has txInfoSignatories :: [PubKeyHash] and adds txInfoObservations :: [Credential], so I suppose we should have both:

• TxInfo.vkKey : ℙ KeyHash (a key-only view used by phase-1/native/timelock parts)
• TxInfo.txGuards : ℙ Credential (full guard/observer set)

but the key point is that vkKey is now derived from txGuards, not stored independently in TxBody.

[williamdemeo]

One more remark about this: maybe the intention of the CIP is that we need "actual signatories" for vkKey (i.e., keys that did sign, from vKeySigs); in that case, this should probably come from witnesses, not from a TxBody "required" field.

UPDATE. Actually, I don't think that's right. I think (in Conway at least) the thing modeled by reqSignerHashes is the "declared/required signers" concept, not "all keys that appear anywhere in witnesses."

When we implement Dijkstra phase-1/timelock/native-script checking, we'll still want a notion of actual witnessed signers (from the witness set / vkey signatures)... but I don't think we'll use vkKey for that (since vkKey is about what scripts see), but rather something computed from witnesses in the validation pipeline...?

[carlostome]

LGTM! Minor comments here and there.

[carlostome]

I'd make this comment part of an admonition that explains how Dijkstra transaction differs from Conway (at the (sub/top) transaction level, not at the level of nested transactions)

[williamdemeo]

I've moved the comments into the prose above the definition.

[carlostome]

Probably this field will have to change to requiredGuards in accordance.

But for now I wouldn't worry too much about txInfo.