Transactions¶
A transaction in Dijkstra is very similar to a transaction in Conway except that now, as described in CIP 01181, it may additionally include
- a list of subtransactions as part of its body; and
- guards, expressed as a set of credentials (key or script), which can be required by scripts and by subtransactions (CIP-0112 / CIP-0118).
Transaction Levels¶
To differentiate between the two types of transactions (i.e. top-level and sub-level), we define the type of transaction level.
data TxLevel : Type where TxLevelTop TxLevelSub : TxLevel
This type will be used, among other purposes, to provide a concise definition of the types of top-level and sub transactions in the Transaction Structure section below.
Transactions cannot be arbitrarily nested. That is, a transaction (henceforth referred
to as a top-level transaction) can include subtransactions, but these cannot include
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 field) and only sub-level transactions
can include required top-level guards (the txRequiredTopLevelGuards field).
To that end, we define two auxiliary functions that will aid in
specifying which record fields of a transaction body are present at
each TxLevel:
InTopLevel : TxLevel → Type → Type InTopLevel TxLevelTop X = X InTopLevel TxLevelSub _ = ⊤ InSubLevel : TxLevel → Type → Type InSubLevel TxLevelSub X = X InSubLevel TxLevelTop _ = ⊤
These functions discriminate on an argument of type
TxLevel and either act as the identity function on types
or as the constant function that returns the unit type.
Transaction Structure¶
record TransactionStructure : Type₁ where field Ix TxId AuxiliaryData : Type adHashingScheme : isHashableSet AuxiliaryData globalConstants : GlobalConstants crypto : CryptoStructure epochStructure : EpochStructure
scriptStructure : ScriptStructure
govParams : GovParams tokenAlgebra : TokenAlgebra txidBytes : TxId → Ser
govStructure : GovStructure govStructure = record -- TODO: figure out what to do with the hash { TxId = TxId; DocHash = ADHash ; cryptoStructure = crypto ; epochStructure = epochStructure ; scriptStructure = scriptStructure ; govParams = govParams ; globalConstants = globalConstants }
TxIn : Type TxIn = TxId × Ix TxOut : Type TxOut = Addr × Value × Maybe (Datum ⊎ DataHash) × Maybe Script UTxO : Type UTxO = TxIn ⇀ TxOut RedeemerPtr : TxLevel → Type RedeemerPtr txLevel = Tag txLevel × Ix ProposedPPUpdates : Type ProposedPPUpdates = KeyHash ⇀ PParamsUpdate Update : Type Update = ProposedPPUpdates × Epoch record HasUTxO {a} (A : Type a) : Type a where field UTxOOf : A → UTxO open HasUTxO ⦃...⦄ public
The Main Transaction Types¶
Transactions are represented as three mutually recursive record types that are
parameterised by a value of type TxLevel.
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: only present in top-level transactions, this field contains the collateral inputs provided to cover script execution costs in case of script failure; -
txFee: only present in top-level transactions, this field contains the fee paid for processing the transaction; -
txSubTransactions: only present in top-level transactions, this field contains a list of sub-transactions included in the top-level transaction; -
txGuards: only present in top-level transactions, this field collects the guard credentials (keys or scripts) required by this transaction and/or by its subtransactions; -
txRequiredTopLevelGuards: only present in sub-level transactions, this field collects the guards (credential, optional datum) required by a subtransaction.
mutual record Tx (txLevel : TxLevel) : Type where inductive field txBody : TxBody txLevel txWitnesses : TxWitnesses txLevel txSize : ℕ isValid : InTopLevel txLevel Bool txAuxData : Maybe AuxiliaryData record TxBody (txLevel : TxLevel) : Type where inductive field txIns : ℙ TxIn referenceInputs : ℙ TxIn collateralInputs : InTopLevel txLevel (ℙ TxIn) txOuts : Ix ⇀ TxOut txId : TxId txCerts : List DCert txFee : InTopLevel txLevel Fees txWithdrawals : Withdrawals txVldt : Maybe Slot × Maybe Slot txADhash : Maybe ADHash txDonation : Donations txGovVotes : List GovVote txGovProposals : List GovProposal txNetworkId : Maybe Network currentTreasury : Maybe Coin mint : Value scriptIntegrityHash : Maybe ScriptHash -- New in Dijkstra -- txSubTransactions : InTopLevel txLevel (List (Tx TxLevelSub)) txGuards : ℙ Credential txRequiredTopLevelGuards : InSubLevel txLevel (ℙ (Credential × Maybe Datum)) --------------------- requiredSignerHashes : ℙ KeyHash requiredSignerHashes = mapPartial isKeyHashObj txGuards record TxWitnesses (txLevel : TxLevel) : Type where inductive field vKeySigs : VKey ⇀ Sig scripts : ℙ Script txData : ℙ Datum txRedeemers : RedeemerPtr txLevel ⇀ Redeemer × ExUnits scriptsP1 : ℙ P1Script scriptsP1 = mapPartial isInj₁ scripts
Using these types, we define the types of top-level and sub transaction as follows:
TopLevelTx : Type TopLevelTx = Tx TxLevelTop SubLevelTx : Type SubLevelTx = Tx TxLevelSub
In addition, we define the type of transactions in which its level could be either of them.
AnyLevelTx : Type AnyLevelTx = TopLevelTx ⊎ SubLevelTx
Auxiliary Functions for Transaction Structures¶
In the Dijkstra era, we need to talk about which UTxO a helper is parameterised by.
- Spending inputs are always inspected against the pre-batch UTxO snapshot (
utxo₀). - Script/data availability is batch-scoped; in the ledger rules, the global
script universe and datum-by-hash pool are computed once per top-level batch
(using
getAllScriptsandgetAllData).
The function getTxScripts defined below is the set of scripts the
ledger may use to resolve script hashes while validating a transaction, given it is
allowed to inspect utxo for its inputs.
-- Helpers -- --| extract scripts from TxOuts txOutToScript : TxOut → Maybe Script txOutToScript (_ , _ , _ , s) = s --| extract datum from TxOuts txOutToDatum : TxOut → Maybe Datum txOutToDatum (_ , _ , d , _) = d >>= isInj₁ --| extract value from TxOuts txOutToValue : TxOut → Value txOutToValue (_ , v , _ , _) = v --| extract set of values from a UTxO valuesOfUTxO : UTxO → ℙ Value valuesOfUTxO = mapˢ txOutToValue ∘ range --| Spending inputs allSpendInputs : TopLevelTx → ℙ TxIn allSpendInputs txTop = foldl (λ acc txSub → acc ∪ SpendInputsOf txSub) (SpendInputsOf txTop) (SubTransactionsOf txTop) allSpendInputsList : TopLevelTx → List (ℙ TxIn) allSpendInputsList t = SpendInputsOf t ∷ map SpendInputsOf (SubTransactionsOf t) --| Reference inputs allReferenceInputs : TopLevelTx → ℙ TxIn allReferenceInputs txTop = foldl (λ acc txSub → acc ∪ ReferenceInputsOf txSub) (ReferenceInputsOf txTop) (SubTransactionsOf txTop) --| OUTPUTS ------------------------------------------------------------------- --| --| Sets of TxOuts can come from the range of... --| --| ...a UTxO _ : UTxO → ℙ TxOut _ = range --| --| ...the txOuts field of a transaction _ : Tx txLevel → ℙ TxOut _ = range ∘ TxOutsOf --| TxOuts from .a UTxO restricted to spending inputs of a Tx spendTxOuts : Tx txLevel → UTxO → ℙ TxOut spendTxOuts tx utxo = range (utxo ∣ SpendInputsOf tx) --| TxOuts from .a UTxO restricted to reference inputs of a Tx referencedTxOuts : Tx txLevel → UTxO → ℙ TxOut referencedTxOuts tx utxo = range (utxo ∣ ReferenceInputsOf tx) --| Set of scripts from outputs of a UTxO scriptsOfUTxO : UTxO → ℙ Script scriptsOfUTxO = mapPartial txOutToScript ∘ range --| Set of scripts from outputs of a Tx scriptsOfTx : Tx txLevel → ℙ Script scriptsOfTx = mapPartial txOutToScript ∘ range ∘ TxOutsOf --| Set of scripts from the spending inputs of a Tx spendScripts : Tx txLevel → UTxO → ℙ Script spendScripts = mapPartial txOutToScript ∘₂ spendTxOuts --| Set of scripts from reference inputs referenceScripts : Tx txLevel → UTxO → ℙ Script referenceScripts = mapPartial txOutToScript ∘₂ referencedTxOuts --| Set of scripts from reference inputs in a batch allReferenceScripts : TopLevelTx → UTxO → ℙ Script allReferenceScripts tx utxo = foldl (λ acc t → acc ∪ referenceScripts t utxo) (referenceScripts tx utxo) (SubTransactionsOf tx) --| Set of scripts from a transactions's witness field witnessScripts : Tx txLevel → ℙ Script witnessScripts = ScriptsOf --| Set of all scripts from a transaction getTxScripts : Tx txLevel → UTxO → ℙ Script getTxScripts tx utxo = scriptsOfTx tx ∪ spendScripts tx utxo ∪ referenceScripts tx utxo ∪ witnessScripts tx --| Set of scripts from a batch getAllScripts : TopLevelTx → UTxO → ℙ Script getAllScripts txTop utxo = foldl (λ acc txSub → acc ∪ getTxScripts txSub utxo) (getTxScripts txTop utxo) (SubTransactionsOf txTop) --| Set of datum from a transaction dataOfTx : Tx txLevel → ℙ Datum dataOfTx = mapPartial txOutToDatum ∘ range ∘ TxOutsOf --| Set of data from a UTxO txOutDataOfUTxO : UTxO → ℙ Datum txOutDataOfUTxO = mapPartial txOutToDatum ∘ range --| Set of data from spendTxOuts spendData : Tx txLevel → UTxO → ℙ Datum spendData = mapPartial txOutToDatum ∘₂ spendTxOuts --| Set of data from referencedTxOuts referenceData : Tx txLevel → UTxO → ℙ Datum referenceData = mapPartial txOutToDatum ∘₂ referencedTxOuts --| Set of data from a transaction's witness field witnessData : Tx txLevel → ℙ Datum witnessData = DataOf --| Set of data from a transaction getTxData : Tx txLevel → UTxO → ℙ Datum getTxData tx utxo = dataOfTx tx ∪ spendData tx utxo ∪ referenceData tx utxo ∪ witnessData tx --| Set of data from a batch getAllData : TopLevelTx → UTxO → ℙ Datum getAllData txTop utxo = foldl (λ acc txSub → acc ∪ getTxData txSub utxo) (getTxData txTop utxo) (SubTransactionsOf txTop) NoOverlappingSpendInputs : TopLevelTx → Type NoOverlappingSpendInputs topTx = List.AllPairs disjoint (SpendInputsOf topTx ∷ map SpendInputsOf (SubTransactionsOf topTx)) -- Total Ada minted across the entire batch (top-level tx + all sub-txs). allMintedCoin : TopLevelTx → Coin allMintedCoin txTop = foldl (λ acc txSub → acc + coin (MintedValueOf txSub)) (coin (MintedValueOf txTop)) (SubTransactionsOf txTop) -- To maintain total Ada supply invariant, this must satisfy `allMintedCoin ≡ 0`; -- this is a generalization of Conway's `coin mint ≡ 0`. lookupScriptHash : ScriptHash → Tx txLevel → UTxO → Maybe Script lookupScriptHash sh tx utxo = lookupHash sh (getTxScripts tx utxo)
CIP-0118 models "required top-level guards" as a list of requirements coming from subtransaction bodies. The list can contain duplicates, and later logic needs to run each distinct guard credential once while still providing it with all arguments (and knowing which subtransaction required them).
Because they are new and their meaning may be slightly less obvious than that of the functions defined above, we'll provide a one-line description for each of the remaining helper functions of this section.
-
TaggedTopLevelGuardis the type of "tagged" top-level guards (tagged by the id of the subtransaction requiring it); an inhabitant ofTaggedTopLevelGuardrepresents a guard as a triple comprised of subtransaction id, guard credential, and optional datum argument; the subtransaction id should be that of the subtransaction requiring the guard. -
GroupedTopLevelGuardsis the type of lists of guard groups, grouped by credential; each element of such a list is a guard credential paired with a list of all subtransaction ids and optional datum arguments requiring that the guard with that credential. (We use a simple association list for now to avoid committing to a particular Map interface.) -
groupTopLevelGuards: a function that takes a list of tagged top-level guards and groups them intoGroupedTopLevelGuardsby folding an insertion function over the list. -
subTxTaggedGuards: a function that takes a subtransaction and produces a set of tagged top-level guards required by that subtransaction, by mapping over itstxRequiredTopLevelGuardsfield and attaching the subtransaction's id to each guard. (We attach the id of the subTx requiring the guard so later execution logic can attribute arguments to the right subtransaction.)
TaggedTopLevelGuard : Type TaggedTopLevelGuard = TxId × Credential × Maybe Datum -- (subTxId, guard credential, optional datum argument) GroupedTopLevelGuards : Type GroupedTopLevelGuards = List (Credential × List (TxId × Maybe Datum)) groupTopLevelGuards : List TaggedTopLevelGuard → GroupedTopLevelGuards groupTopLevelGuards = foldr insertGuard [] where -- Insert one tagged guard into an existing group: -- + if the credential already has a group, cons (subTxId, datum?) onto its list -- + otherwise create a new group for that credential. insertGuard : TaggedTopLevelGuard → GroupedTopLevelGuards → GroupedTopLevelGuards insertGuard (tid , cred , md) [] = (cred , (tid , md) ∷ []) ∷ [] insertGuard (tid , cred , md) ((c , xs) ∷ rest) with c ≟ cred ... | yes _ = (c , (tid , md) ∷ xs) ∷ rest ... | no _ = (c , xs) ∷ insertGuard (tid , cred , md) rest subTxTaggedGuards : SubLevelTx → ℙ TaggedTopLevelGuard subTxTaggedGuards subtx = mapˢ (λ (cred , md) → (TxIdOf subtx , cred , md)) (TopLevelGuardsOf subtx) -- Turn a subTx body's `txRequiredTopLevelGuards` into a set of guard credentials. subTxGuardCredentials : SubLevelTx → ℙ Credential subTxGuardCredentials = (mapˢ proj₁) ∘ TopLevelGuardsOf -- Phase-1 condition (CIP-0118): -- every credential required by a subTx body must appear in the top-level txGuards set. requiredGuardsInTopLevel : TopLevelTx → List SubLevelTx → Type requiredGuardsInTopLevel topTx subTxs = requiredCreds ⊆ GuardsOf topTx where -- union a list of sets concatMapˡ : {A B : Type} → (A → ℙ B) → List A → ℙ B concatMapˡ f as = proj₁ $ unions (fromList (map f as)) -- maybe move this to agda-sets or src-lib-exts requiredCreds : ℙ Credential requiredCreds = concatMapˡ subTxGuardCredentials subTxs
Changes to Transaction Validity¶
As discussed in [Ledger.Conway.Specification.Properties][], transaction validity is tricky, and this remains true in the Dijkstra era.
The Dijkstra era introduces nested transactions (a single top-level transaction that contains a list of sub-transactions) and guards (CIP-0112 / CIP-0118). As a result, several checks that were "per-transaction" in Conway become batch-aware.
Design Note (spending inputs vs reference inputs).
For Dijkstra batches, we distinguish spending inputs from reference inputs.
All spending inputs across the whole batch must exist in the initial UTxO snapshot.
Reference inputs are treated separately by the UTxO rules. For script/data
availability, the ledger computes batch-wide globalScripts and globalData once
per top-level batch and threads them through the environment, so phase-2 execution
can be done with a shared, batch-scoped witness pool.
Key points¶
-
No further nesting
Sub-transactions must not contain sub-transactions; only a top-level transaction may carry a list of sub-transactions.
-
Collateral is top-level only and mandatory
Sub-transactions do not carry collateral inputs. A top-level transaction must provide sufficient collateral for all scripts that are run as part of validating all transactions in that batch. If any script in the batch fails, then the collateral is collected and none of the transactions in the batch is applied.
-
Batch-wide phase-2 evaluation
Phase-2 (Plutus) validation is performed once for the whole batch, even though script inputs/contexts are constructed from both sub- and top-level components.
-
Guards are credentials
A transaction body may specify guards as a set of credentials (key or script). This is distinct from the legacy "required signer" key hashes used for phase-1 key-witness checking and native/timelock scripts.
-
Required top-level guards are requests
Sub-transaction bodies may include a list of "required top-level guard" requests (credential plus optional datum). Ledger phase-1 checks must ensure that the top-level
guardsincludes all credentials required by sub-transactions before any of the batch transactions are applied. -
The batch must be balanced
Preservation of value (POV) must hold. The updated
producedandconsumedcalculations sum up the appropriate quantities not for individual transactions, but for the entire batch, which includes the top-level transaction and all its sub-transactions. -
Fees / preservation-of-value may become batch-wide
Several accounting checks (e.g. min-fee, preservation of value) are expected to be defined over the full batch rather than per sub-transaction. The definitive statement lives in the Dijkstra UTxO transition once introduced. (At present, Dijkstra keeps
txFeeon the top-level body.) -
Size bounds apply to the whole batch
The size of the top-level transaction (including all its sub-transactions) must be less than
maxTxSize. This constraint is necessary to ensure efficient network operation and preserve performance. -
Scripts/data availability is batch-scoped
The witness set (scripts, redeemers, datums) is considered at the level of the whole top-level transaction/batch. (The exact constraints on what may be referenced are defined by the UTxO rules.)
-
See CIP 0118; once finalized and merged, CIP 0118 will appear in the main branch of the CIP repository; until then, it can be found at https://github.com/polinavino/CIPs/tree/polina/CIP0118/CIP-0118. ↩