Addresses

This section is part of the Ledger.Conway.Specification.Address module of the formal ledger specification, in which we define credentials and various types of addresses here.

A credential contains a hash, either of a verifying (public) key (isVKey) or of a script (isScript).

N.B. in the Shelley era the type of the stake field of the BaseAddr record was CredentialType (see CVG19, ); to specify an address with no stake, we would use an “enterprise” address. In contrast, the type of stake in the Conway era is Maybe CredentialType, so we can now use BaseAddr to specify an address with no stake by setting stake to nothing.

{-# OPTIONS --safe #-}

open import Ledger.Prelude

open import Tactic.Derive.Show

module Ledger.Core.Specification.Address (

Definitions used in Addresses

Abstract types

  Network
  KeyHash
  ScriptHash

  : Type)  ⦃ _ : DecEq Network ⦄ ⦃ _ : DecEq KeyHash ⦄ ⦃ _ : DecEq ScriptHash ⦄ where

Derived types

data Credential : Type where
  KeyHashObj : KeyHash → Credential
  ScriptObj  : ScriptHash → Credential

record HasCredential {a} (A : Type a) : Type a where 
  field CredentialOf : A → Credential
open HasCredential ⦃...⦄ public

isKeyHashObj : Credential → Maybe KeyHash
isKeyHashObj (KeyHashObj h) = just h
isKeyHashObj (ScriptObj _)  = nothing

isKeyHashObjᵇ : Credential → Bool
isKeyHashObjᵇ (KeyHashObj _) = true
isKeyHashObjᵇ _ = false

isKeyHash : Credential → Type
isKeyHash x = isKeyHashObjᵇ x ≡ true

isScriptObj : Credential → Maybe ScriptHash
isScriptObj (KeyHashObj _) = nothing
isScriptObj (ScriptObj h)  = just h

data isVKey : Credential → Type where
  VKeyisVKey : (kh : KeyHash) → isVKey (KeyHashObj kh)

data isScript : Credential → Type where
  SHisScript : (sh : ScriptHash) → isScript (ScriptObj sh)

record BaseAddr : Type where
  field net    : Network
        pay    : Credential
        stake  : Maybe Credential

record BootstrapAddr : Type where
  field net        : Network
        pay        : Credential
        attrsSize  : ℕ

record RwdAddr : Type where
  field net    : Network
        stake  : Credential

Withdrawals : Type
Withdrawals  = RwdAddr ⇀ Coin

open BaseAddr; open BootstrapAddr; open BaseAddr; open BootstrapAddr

record HasNetworkId {a} (A : Type a) : Type a where
  field NetworkIdOf : A → Network
open HasNetworkId ⦃...⦄ public

record HasWithdrawals {a} (A : Type a) : Type a where
  field WithdrawalsOf : A → Withdrawals
open HasWithdrawals ⦃...⦄ public

instance
  HasNetworkId-BaseAddr : HasNetworkId BaseAddr
  HasNetworkId-BaseAddr .NetworkIdOf = BaseAddr.net

  HasNetworkId-BootstrapAddr : HasNetworkId BootstrapAddr
  HasNetworkId-BootstrapAddr .NetworkIdOf = BootstrapAddr.net

  HasNetworkId-RwdAddr : HasNetworkId RwdAddr
  HasNetworkId-RwdAddr .NetworkIdOf = RwdAddr.net

  HasCredential-RwdAddr : HasCredential RwdAddr
  HasCredential-RwdAddr .CredentialOf = RwdAddr.stake

VKeyBaseAddr         = Σ[ addr ∈ BaseAddr       ] isVKey    (addr .pay)
VKeyBootstrapAddr    = Σ[ addr ∈ BootstrapAddr  ] isVKey    (addr .pay)
ScriptBaseAddr       = Σ[ addr ∈ BaseAddr       ] isScript  (addr .pay)
ScriptBootstrapAddr  = Σ[ addr ∈ BootstrapAddr  ] isScript  (addr .pay)

Addr        = BaseAddr        ⊎ BootstrapAddr
VKeyAddr    = VKeyBaseAddr    ⊎ VKeyBootstrapAddr
ScriptAddr  = ScriptBaseAddr  ⊎ ScriptBootstrapAddr

Helper functions

payCred       : Addr → Credential
stakeCred     : Addr → Maybe Credential
netId         : Addr → Network
isVKeyAddr    : Addr → Type
isScriptAddr  : Addr → Type

isVKeyAddr       = isVKey ∘ payCred
isScriptAddr     = isScript ∘ payCred
isScriptRwdAddr  = isScript ∘ CredentialOf

payCred (inj₁ record {pay = pay}) = pay
payCred (inj₂ record {pay = pay}) = pay

stakeCred (inj₁ record {stake = stake}) = stake
stakeCred (inj₂ _) = nothing

netId (inj₁ record {net = net}) = net
netId (inj₂ record {net = net}) = net

data isBootstrapAddr : Addr → Set where
 IsBootstrapAddr : ∀ a → isBootstrapAddr (inj₂ a)

instance
  isBootstrapAddr? : ∀ {a} → isBootstrapAddr a ⁇
  isBootstrapAddr? {inj₁ _} = ⁇ no λ ()
  isBootstrapAddr? {inj₂ a} = ⁇ yes (IsBootstrapAddr a)

instance
  unquoteDecl DecEq-Credential = derive-DecEq ((quote Credential , DecEq-Credential) ∷ [])

  Dec-isVKey : isVKey ⁇¹
  Dec-isVKey {x = c} .dec with c
  ... | KeyHashObj h = yes (VKeyisVKey h)
  ... | ScriptObj  _ = no  λ ()

  Dec-isScript : isScript ⁇¹
  Dec-isScript {x = x} .dec with x
  ... | KeyHashObj _ = no λ ()
  ... | ScriptObj  y = yes (SHisScript y)

_ = isVKey ⁇¹ ∋ it
_ = isVKeyAddr ⁇¹ ∋ it
_ = isScript ⁇¹ ∋ it
_ = isScriptAddr ⁇¹ ∋ it
_ = isScriptRwdAddr ⁇¹ ∋ it

getScriptHash : ∀ a → isScriptAddr a → ScriptHash
getScriptHash (inj₁ _) (SHisScript sh) = sh
getScriptHash (inj₂ _) (SHisScript sh) = sh

instance abstract
  unquoteDecl DecEq-BaseAddr DecEq-BootstrapAddr DecEq-RwdAddr = derive-DecEq
    ( (quote BaseAddr      , DecEq-BaseAddr)
    ∷ (quote BootstrapAddr , DecEq-BootstrapAddr)
    ∷ (quote RwdAddr       , DecEq-RwdAddr)
    ∷ [] )

module _ ⦃ _ : Show Network  ⦄ ⦃ _ : Show KeyHash  ⦄ ⦃ _ : Show ScriptHash  ⦄ where
  instance
    unquoteDecl Show-Credential = derive-Show [ (quote Credential , Show-Credential) ]
    unquoteDecl Show-RwdAddr = derive-Show [ (quote RwdAddr , Show-RwdAddr) ]
    Show-Credential×Coin : Show (Credential × Coin)
    Show-Credential×Coin = Show-×

References

[CVG19] Jared Corduan and Polina Vinogradova and Matthias Güdemann. A Formal Specification of the Cardano Ledger. 2019.