Transactions¶
A transaction in Dijkstra is very similar to a transaction in Conway except that now, as described in CIP 01181, it may include
- other (sub)transactions as part of its body;
- guard scripts.
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 refered
as 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 scripts (credentials) required by this transaction; -
txRequiredTopLevelGuards: only present in sub-level transactions, this field collects the top-level guards required by a subtransaction.
mutual record Tx (txLevel : TxLevel) : Type where inductive field txBody : TxBody txLevel txWitnesses : TxWitnesses txLevel isValid : InTopLevel txLevel Bool txAuxData : Maybe AuxiliaryData record TxBody (txLevel : TxLevel) : Type where inductive field txIns : ℙ TxIn refInputs : ℙ 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)) --------------------- reqSignerHashes : ℙ KeyHash reqSignerHashes = 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¶
This section collects some unimportant but useful helper and accessor functions.
getValue : TxOut → Value getValue (_ , v , _) = v TxOutʰ : Type TxOutʰ = Addr × Value × Maybe (Datum ⊎ DataHash) × Maybe ScriptHash txOutHash : TxOut → TxOutʰ txOutHash (a , v , d , s) = a , (v , (d , M.map hash s)) getValueʰ : TxOutʰ → Value getValueʰ (_ , v , _) = v txinsVKey : ℙ TxIn → UTxO → ℙ TxIn txinsVKey txins utxo = txins ∩ dom (utxo ∣^' (isVKeyAddr ∘ proj₁)) scriptOuts : UTxO → UTxO scriptOuts utxo = filter (λ (_ , addr , _) → isScriptAddr addr) utxo txinsScript : ℙ TxIn → UTxO → ℙ TxIn txinsScript txins utxo = txins ∩ dom (proj₁ (scriptOuts utxo))
In the Dijkstra era, spending inputs must exist in the initial UTxO snapshot, while reference inputs may come from earlier outputs, so we will need two to keep track of two UTxOs; we'll denote these as follows:
utxo₀, the initial UTxO snapshot, used fortxIns;utxoRef, the evolving UTxO, used for reference input lookups.
We now define some functions for scripts. Some of these will take two UTxO
arguments, denoting the initial UTxO snapshot and an evolving UTxO, which evolves as
a batch of subtransactions is processed. (Later, when the functions below are used,
the two UTxO arguments may come from the UTxO environment and an evolving UTxO state;
types for these are defined in the Utxo module, which depends
on the present module; thus, we cannot bind the UTxO arguments to a particular
UTxO environment and state at this point.)
txOutToScript : TxOut → Maybe Script txOutToScript (_ , _ , _ , s) = s getTxScripts : UTxO → Tx txLevel → ℙ Script getTxScripts utxo tx = ScriptsOf tx -- (1) scripts from witnesses ∪ mapPartial txOutToScript ( range (utxo ∣ SpendInputsOf tx) -- (2) scripts from spending inputs ∪ range (utxo ∣ ReferenceInputsOf tx) -- (3) scripts from reference inputs ∪ range (TxOutsOf tx ˢ)) -- (4) scripts from transaction outputs getAllScripts : TopLevelTx → UTxO → ℙ P1Script × ℙ P2Script getAllScripts tx utxo = mapPartial toP1Script allScripts , mapPartial toP2Script allScripts where allScripts : ℙ Script allScripts = getTxScripts utxo tx -- (1) scripts from top-level transaction ∪ concatMapˢ (getTxScripts utxo) (fromList (SubTransactionsOf tx)) -- (2) scripts from subtransactions lookupScriptHash : ScriptHash → Tx txLevel → UTxO → UTxO → Maybe Script lookupScriptHash sh tx utxoSpend₀ utxoRefView = lookupHash sh (getTxScripts utxoRefView tx) txOutToDatum : TxOut → Maybe Datum txOutToDatum (_ , _ , d , _) = d >>= isInj₁ getTxData : UTxO → Tx txLevel → ℙ Datum getTxData utxo tx = DataOf tx -- (1) data from witnesses ∪ mapPartial txOutToDatum ( range (utxo ∣ SpendInputsOf tx) -- (2) data from spending inputs ∪ range (utxo ∣ ReferenceInputsOf tx) -- (3) data from reference inputs ∪ range (TxOutsOf tx ˢ)) -- (4) data from transaction outputs getAllData : TopLevelTx → UTxO → ℙ Datum getAllData tx utxo = getTxData utxo tx ∪ concatMapˢ (getTxData utxo) (fromList (SubTransactionsOf tx))
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. -
subTxTopLevelGuards: 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. requiredTopLevelGuardsSatisfied : TopLevelTx → List SubLevelTx → Type requiredTopLevelGuardsSatisfied topTx subTxs = requiredCreds ⊆ GuardsOf topTx where concatMapˡ : {A B : Type} → (A → ℙ B) → List A → ℙ B concatMapˡ f as = proj₁ $ unions (fromList (map f as)) -- (maybe move concatMapˡ to src-lib-exts or agda-sets) 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 (CIP-0118: 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 (mempool safety). Reference inputs may additionally point to outputs of preceding subtransactions in the batch order. Therefore reference-script/datum lookup is performed against an evolving, tentative UTxO view (prefix-applied), used only for lookup/validation, while ledger state is committed only if the full batch succeeds.
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 (mempool safety), 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. ↩