Utxow

Witnessing

This section is part of the Ledger.Conway.Utxow module of the formal ledger specification, in which we define witnessing.

The purpose of witnessing is make sure the intended action is authorized by the holder of the signing key. (For details see .) Figure 'Functions-used-for-witnessing' defines functions used for witnessing. witsVKeyNeeded and scriptsNeeded are now defined by projecting the same information out of credsNeeded. Note that the last component of credsNeeded adds the script in the proposal policy only if it is present.

{-# OPTIONS --safe #-}

open import Ledger.Prelude
open import Ledger.Conway.Crypto
open import Ledger.Conway.Abstract
open import Ledger.Conway.Transaction

module Ledger.Conway.Utxow
  (txs : _) (open TransactionStructure txs)
  (abs : AbstractFunctions txs) (open AbstractFunctions abs)
  where
open import Ledger.Conway.Utxo txs abs
open import Ledger.Conway.Script.Validation txs abs
open import Ledger.Conway.Certs govStructure

allowedLanguages has additional conditions for new features in Conway. If a transaction contains any votes, proposals, a treasury donation or asserts the treasury amount, it is only allowed to contain Plutus V3 scripts. Additionally, the presence of reference scripts or inline scripts does not prevent Plutus V1 scripts from being used in a transaction anymore. Only inline datums are now disallowed from appearing together with a Plutus V1 script.

Functions used for witnessing

module _ (o : TxOut) where
  d = proj₁ (proj₂ (proj₂ o))
  data HasInlineDatum : Set where
    InlineDatum  : ∀ {d'} → d ≡ just (inj₁ d') → HasInlineDatum

instance
  Dec-HasInlineDatum : ∀ {o} → HasInlineDatum o ⁇
  Dec-HasInlineDatum {_ , _ , just (inj₁ x) , _} = ⁇ yes (InlineDatum refl)
  Dec-HasInlineDatum {_ , _ , just (inj₂ x) , _} = ⁇ no λ where
    (InlineDatum x) → case x of λ ()
  Dec-HasInlineDatum {_ , _ , nothing , _} = ⁇ no λ where
    (InlineDatum x) → case x of λ ()

module _ (txb : TxBody) (let open TxBody txb) where
  data UsesV3Features : Set where
    HasVotes : txvote ≢ [] → UsesV3Features
    HasProps : txprop ≢ [] → UsesV3Features
    HasDonation : txdonation ≢  → UsesV3Features
    HasTreasury : curTreasury ≢ nothing → UsesV3Features

instance
  Dec-UsesV3Features : ∀ {txb} → UsesV3Features txb ⁇
  Dec-UsesV3Features {record { txvote = [] ; txprop = [] ; txdonation = zero ; curTreasury = nothing }}
    = ⁇ no λ where (HasVotes x)    → x refl
                   (HasProps x)    → x refl
                   (HasDonation x) → x refl
                   (HasTreasury x) → x refl
  Dec-UsesV3Features {record { txvote = [] ; txprop = [] ; txdonation = zero ; curTreasury = just x }}
    = ⁇ yes (HasTreasury (λ ()))
  Dec-UsesV3Features {record { txvote = [] ; txprop = [] ; txdonation = suc txdonation }}
    = ⁇ yes (HasDonation (λ ()))
  Dec-UsesV3Features {record { txvote = [] ; txprop = x ∷ txprop }} = ⁇ yes (HasProps (λ ()))
  Dec-UsesV3Features {record { txvote = x ∷ txvote }} = ⁇ yes (HasVotes (λ ()))

languages : Tx → UTxO → ℙ Language
languages tx utxo = mapPartial getLanguage (txscripts tx utxo)
  where
    getLanguage : Script → Maybe Language
    getLanguage (inj₁ _) = nothing
    getLanguage (inj₂ s) = just (language s)

allowedLanguages : Tx → UTxO → ℙ Language
allowedLanguages tx utxo =
  if (∃[ o ∈ os ] isBootstrapAddr (proj₁ o))
    then ∅
  else if UsesV3Features txb
    then fromList (PlutusV3 ∷ [])
  else if ∃[ o ∈ os ] HasInlineDatum o
    then fromList (PlutusV2 ∷ PlutusV3 ∷ [])
  else
    fromList (PlutusV1 ∷ PlutusV2 ∷ PlutusV3 ∷ [])
  where
    txb = tx .Tx.body; open TxBody txb
    os = range (outs txb) ∪ range (utxo ∣ (txins ∪ refInputs))

UTxOW transition system types

data

  _⊢_⇀⦇_,UTXOW⦈_ : UTxOEnv → UTxOState → Tx → UTxOState → Type

UTXOW inference rules

private variable
  Γ           : UTxOEnv
  s s'        : UTxOState
  tx          : Tx

open UTxOState

data _⊢_⇀⦇_,UTXOW⦈_ where

  UTXOW-inductive :
    let  utxo                                = s .utxo

         open Tx tx renaming (body to txb); open TxBody txb; open TxWitnesses wits

         witsKeyHashes                       = mapˢ hash (dom vkSigs)
         witsScriptHashes                    = mapˢ hash scripts
         refScriptHashes                     = mapˢ hash (refScripts tx utxo)
         neededScriptHashes                  = mapPartial (isScriptObj  ∘ proj₂) (credsNeeded utxo txb)
         neededVKeyHashes                    = mapPartial (isKeyHashObj ∘ proj₂) (credsNeeded utxo txb)
         txdatsHashes                        = mapˢ hash txdats
         inputsDataHashes                    = mapPartial (λ txout → if txOutToP2Script utxo tx txout
                                                                      then txOutToDataHash txout
                                                                      else nothing) (range (utxo ∣ txins))
         refInputsDataHashes                 = mapPartial txOutToDataHash (range (utxo ∣ refInputs))
         outputsDataHashes                   = mapPartial txOutToDataHash (range txouts)
         nativeScripts                       = mapPartial toP1Script (txscripts tx utxo)

    in
    ∙  ∀[ (vk , σ) ∈ vkSigs ] isSigned vk (txidBytes txid) σ
    ∙  ∀[ s ∈ nativeScripts ] (hash s ∈ neededScriptHashes → validP1Script witsKeyHashes txvldt s)
    ∙  neededVKeyHashes ⊆ witsKeyHashes
    ∙  neededScriptHashes - refScriptHashes ≡ᵉ witsScriptHashes
    ∙  inputsDataHashes ⊆ txdatsHashes
    ∙  txdatsHashes ⊆ inputsDataHashes ∪ outputsDataHashes ∪ refInputsDataHashes
    ∙  languages tx utxo ⊆ allowedLanguages tx utxo
    ∙  txADhash ≡ map hash txAD
    ∙  Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s'
       ────────────────────────────────
       Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s'

pattern UTXOW-inductive⋯ p₁ p₂ p₃ p₄ p₅ p₆ p₇ p₈ h
      = UTXOW-inductive (p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , h)
pattern UTXOW⇒UTXO x = UTXOW-inductive⋯ _ _ _ _ _ _ _ _ x

unquoteDecl UTXOW-inductive-premises =
  genPremises UTXOW-inductive-premises (quote UTXOW-inductive)

Plutus script context

CIP-0069 unifies the arguments given to all types of Plutus scripts currently available: spending, certifying, rewarding, minting, voting, proposing.

The formal specification permits running spending scripts in the absence datums in the Conway era. However, since the interface with Plutus is kept abstract in this specification, changes to the representation of the script context which are part of CIP-0069 are not included here. To provide a CIP-0069-conformant implementation of Plutus to this specification, an additional step processing the List Data argument we provide would be required.

In Figure 'UTXOW-inference-rules', the line inputHashes subseteqfield txdatsHashes compares two inhabitants of PowerSet DataHash. In the Alonzo spec, these two terms would have inhabited PowerSet (Maybe DataHash), where a nothing is thrown out .