Skip to content

[Dijkstra] TxBody replace txRequiredGuards #1008

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
williamdemeo merged 6 commits into from
Jan 7, 2026
+79 −37
Merged

[Dijkstra] TxBody replace txRequiredGuards #1008

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
b2537a7
Replace `txRequiredGuards` -> credential `txGuards`
williamdemeo Dec 18, 2025
42d5615
improve readability in `txInfo` assignments ...
williamdemeo Dec 19, 2025
7871e93
update CHANGELOG
williamdemeo Dec 19, 2025
1cab986
address Carlos's point, avoiding duplication
williamdemeo Jan 6, 2026
f51045f
fix comments and hide boilerplate from web docs
williamdemeo Jan 7, 2026
6a4b59e
Address PR change requests
williamdemeo Jan 7, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 6 additions & 1 deletion CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,14 @@
# Changelog

## Conway spec
## Dijkstra spec

### WIP

- Change `TxBody.txRequiredGuards` to `TxBody.txGuards`.
- Add `TxBody.reqSignerHashes`.

## Conway spec

- Change `RwdAddr` to `RewardAddress`
- Do not count pool deposits a second time when reregistering pools
- Allow reregistration of pools in the POOL transition relation
Expand Down
5 changes: 5 additions & 0 deletions src/Ledger/Conway/Specification/Abstract.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ source_branch: master
source_path: src/Ledger/Conway/Specification/Abstract.lagda.md
---

<!--
```agda
{-# OPTIONS --safe #-}

Expand All @@ -14,7 +15,10 @@ module Ledger.Conway.Specification.Abstract (txs : TransactionStructure) where
open TransactionStructure txs
open import Ledger.Conway.Specification.Certs govStructure
open import Ledger.Conway.Specification.Script.ScriptPurpose txs
```
-->

```agda
record indexOf : Type where
field
indexOfDCert : DCert → List DCert → Maybe Ix
Expand All @@ -31,3 +35,4 @@ record AbstractFunctions : Type where
runPLCScript : CostModel → P2Script → ExUnits → List Data → Bool
scriptSize : Script → ℕ
valContext : TxInfo → ScriptPurpose → Data
```
5 changes: 4 additions & 1 deletion src/Ledger/Conway/Specification/Script/Base.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ source_branch: master
source_path: src/Ledger/Conway/Specification/Script/Base.lagda.md
---

<!--
```agda
{-# OPTIONS --safe #-}

Expand All @@ -13,7 +14,6 @@ open import Data.Nat.Properties using (+-0-commutativeMonoid; suc-injective)

open import stdlib.Data.List.Relation.Unary.MOf


open import Ledger.Prelude hiding (All; Any; all?; any?; _∷ʳ_; uncons; _⊆_)
open import Ledger.Core.Specification.Crypto
open import Ledger.Core.Specification.Epoch
Expand All @@ -22,7 +22,10 @@ module Ledger.Conway.Specification.Script.Base
(cs : _) (open CryptoStructure cs)
(es : _) (open EpochStructure es)
where
```
-->

```agda
record P1ScriptStructure : Type₁ where
field P1Script : Type
validP1Script : ℙ KeyHash → Maybe Slot × Maybe Slot → P1Script → Type
Expand Down
49 changes: 26 additions & 23 deletions src/Ledger/Dijkstra/Specification/Script/Validation.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,38 +72,41 @@ record TxInfo : Type where
txCerts : List DCert
txWithdrawals : Withdrawals
txVldt : Maybe Slot × Maybe Slot
vkKey : ℙ KeyHash
vkKey : ℙ KeyHash -- native/phase-1/timelock signers
txGuards : ℙ Credential -- CIP-0112/0118 guards (required by tx body)
txData : ℙ Datum
txId : TxId


txInfo : (ℓ : TxLevel) → UTxO → Tx ℓ → TxInfo

txInfo TxLevelTop utxo tx =
record { realizedInputs = utxo ∣ txIns
; txOuts = txOuts
; txFee = just txFee
; mint = mint
; txCerts = txCerts
; txWithdrawals = txWithdrawals
; txVldt = txVldt
; vkKey = txRequiredGuards -- ?
; txData = DataOf tx
; txId = txId
} where open Tx tx; open TxBody txBody
record { realizedInputs = utxo ∣ (TxBody.txIns txBody)
; txOuts = TxBody.txOuts txBody
; txFee = just (TxBody.txFee txBody)
; mint = TxBody.mint txBody
; txCerts = TxBody.txCerts txBody
; txWithdrawals = TxBody.txWithdrawals txBody
; txVldt = TxBody.txVldt txBody
; vkKey = TxBody.reqSignerHashes txBody
Copy link
Collaborator

@carlostome carlostome Jan 7, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

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

; txGuards = TxBody.txGuards txBody
; txData = DataOf tx
; txId = TxBody.txId txBody
} where open Tx tx

txInfo TxLevelSub utxo tx =
record { realizedInputs = utxo ∣ txIns
; txOuts = txOuts
; txFee = nothing
; mint = mint
; txCerts = txCerts
; txWithdrawals = txWithdrawals
; txVldt = txVldt
; vkKey = txRequiredGuards -- ?
; txData = DataOf tx
; txId = txId
} where open Tx tx; open TxBody txBody
record { realizedInputs = utxo ∣ (TxBody.txIns txBody)
; txOuts = TxBody.txOuts txBody
; txFee = nothing
; mint = TxBody.mint txBody
; txCerts = TxBody.txCerts txBody
; txWithdrawals = TxBody.txWithdrawals txBody
; txVldt = TxBody.txVldt txBody
; vkKey = TxBody.reqSignerHashes txBody
; txGuards = TxBody.txGuards txBody
; txData = DataOf tx
; txId = TxBody.txId txBody
} where open Tx tx
```

<!--
Expand Down
50 changes: 38 additions & 12 deletions src/Ledger/Dijkstra/Specification/Transaction.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,7 +52,11 @@ section below.

Transactions cannot be arbitrarily nested. That is, a transaction (henceforth refered
as top-level transaction) can include subtransactions, but these cannot include
other subtransactions.
other subtransactions. This will manifest in the types of transactions defined
below by constraining which fields are present in each level of transaction.
Specifically, only top-level transactions can include subtransactions
(the `txSubTransactions`{.AgdaField} field) and only sub-level transactions
can include required top-level guards (the `txRequiredTopLevelGuards`{.AgdaField} field).

To that end, we define two auxiliary functions that will aid in
specifying which record fields of a transaction body are present at
Expand Down Expand Up @@ -178,12 +182,33 @@ record TransactionStructure : Type₁ where
open HasUTxO ⦃...⦄ public
```

The type of transactions is defined as three mutually recursive
records parameterised by a value of type `TxLevel`{.agdatype}.
## The Main Transaction Types

Transactions are represented as three mutually recursive record types that are
parameterised by a value of type `TxLevel`{.agdatype}.

The fields that depend on the transaction level use the auxiliary functions
`InTopLevel` and `InSubLevel` defined in the section on [Transaction Levels][].

Of particular note in the Dijkstra era are

+ `collateralInputs`{.AgdaField}: only present in top-level transactions,
this field contains the collateral inputs provided to cover script execution
costs in case of script failure;

+ `txFee`{.AgdaField}: only present in top-level transactions,
this field contains the fee paid for processing the transaction;

+ `txSubTransactions`{.AgdaField}: only present in top-level transactions,
this field contains a list of sub-transactions included in the top-level
transaction;

+ `txGuards`{.AgdaField}: only present in top-level transactions,
this field collects the guard scripts (credentials) required by this transaction;

+ `txRequiredTopLevelGuards`{.AgdaField}: only present in sub-level transactions,
this field collects the top-level guards required by a subtransaction.

```agda
mutual
record Tx (txLevel : TxLevel) : Type where
Expand All @@ -199,11 +224,11 @@ The fields that depend on the transaction level use the auxiliary functions
field
txIns : ℙ TxIn
refInputs : ℙ TxIn
collateralInputs : InTopLevel txLevel (ℙ TxIn) -- only in top-level tx
collateralInputs : InTopLevel txLevel (ℙ TxIn)
txOuts : Ix ⇀ TxOut
txId : TxId
txCerts : List DCert
txFee : InTopLevel txLevel Fees -- only in top-level tx
txFee : InTopLevel txLevel Fees
txWithdrawals : Withdrawals
txVldt : Maybe Slot × Maybe Slot
txADhash : Maybe ADHash
Expand All @@ -216,15 +241,16 @@ The fields that depend on the transaction level use the auxiliary functions
scriptIntegrityHash : Maybe ScriptHash

-- New in Dijkstra --
--
txSubTransactions : InTopLevel txLevel (List (Tx TxLevelSub)) -- only in top-level tx
-- ^^^^^^^^^^ should this be a set? i.e. InTopLevel txLevel (ℙ (Tx TxLevelSub))
-- (in getTxScripts function below we need it as a set)
--
txRequiredGuards : ℙ KeyHash -- replaces reqSigHash : ℙ KeyHash
txRequiredTopLevelGuards : InSubLevel txLevel (ScriptHash ⇀ Datum) -- only in sub-level tx
txSubTransactions : InTopLevel txLevel (List (Tx TxLevelSub))
txGuards : ℙ Credential
txRequiredTopLevelGuards : InSubLevel txLevel (ScriptHash ⇀ Datum)
-- ^ TODO (CIP-0118): change to ℙ (Credential × Maybe Datum)
---------------------

reqSignerHashes : ℙ KeyHash
reqSignerHashes = mapPartial isKeyHashObj txGuards


record TxWitnesses (txLevel : TxLevel) : Type where
inductive
field
Expand Down