🚧 Work In Progress — DO NOT USE in production 🚧

The Cardano Deposit Wallet is a full-node wallet targeting businesses that need to track the origin of incoming payments ("deposits").

This page documents the Cardano Deposit Wallet software.

Use the sidebar for navigation.

• Installation — Installation instructions. You need to do this in order to run the software.
• Examples — Usage examples. Read this to get started.
• Usage — User manual for the software.
• API — API reference.
• Design — Design documents. Read this for a precise understanding of what the wallet does and why.
• Contributing — Information for people who want to work with and contribute to the code.

Installation

This document describes how to install and start the Cardano Deposit Wallet.

The instructions in this document are tested automatically as part of our continuous integration.

System Prerequisites

This is a full node experience, so all the caveats of running a full node apply.

In particular, for mainnet you will need:

• 24 GB RAM (UTxO set is still in memory)
• 250 GB disk space (Transaction history is stored in full)
• 4 CPU cores (for syncing)

But for preprod, you can get away with:

• 2 GB RAM
• 5 GB disk space
• 2 CPU cores

You will need some tools to complete the installation:

• jq
• wget
• curl
• tar
• screen
• a working browser

Nix users can run a shell with all the tools:

nix-shell -p jq wget gnutar screen curl

or

nix shell nixpkgs#jq nixpkgs#wget nixpkgs#gnutar nixpkgs#screen nixpkgs#curl

We are going to use the preprod network in these instructions. Small changes are needed to run on other networks.

Create a directory for the node state or use the current directory

NODE_DB=${NODE_DB:-$(pwd)/node-db}
export NODE_DB
mkdir -p "$NODE_DB"
rm -rf "$NODE_DB/preprod"

Now you have two choices on how to proceed:

Use a package for your system.

Not all platforms are supported, but we have packages for linux64, macos-silicon, and macos-intel.

• Using a platform package. As we do not ship for Windows, you will have to use a Docker solution.

Using a docker image

The Docker image is built through the Nix package manager and has no base image.

• Using a docker image

Download the Mithril executable

case $PACKAGED_FOR in
    linux64)
        MITHRIL_PLATFORM=linux-x64
        ;;
    macos-silicon)
        MITHRIL_PLATFORM=macos-arm64
        ;;
    macos-intel)
        MITHRIL_PLATFORM=macos-x64
        ;;
    *)
        echo "Unsupported platform: $PACKAGED_FOR"
        exit 1
        ;;
esac
LATEST_MITHRIL=$(curl -s https://api.github.com/repos/input-output-hk/mithril/releases/latest | jq -r .tag_name)
MITHRIL_NAME=mithril-$LATEST_MITHRIL-$MITHRIL_PLATFORM
wget -q https://github.com/input-output-hk/mithril/releases/download/$LATEST_MITHRIL/$MITHRIL_NAME.tar.gz
MITHRIL_DIR=$(pwd)/$MITHRIL_NAME
mkdir -p "$MITHRIL_DIR"
tar xvzf "$MITHRIL_NAME.tar.gz" -C "$MITHRIL_DIR" > /dev/null
rm -f "$MITHRIL_NAME.tar.gz"
export PATH="$MITHRIL_DIR":$PATH

Test that mithril is installed correctly by running mithril --version.

mithril-client --version

NixOS will refuse to run Mithril unless programs.nix-ld.enable = true; is in the configuration.

Populate the node state with preprod data

export AGGREGATOR_ENDPOINT=https://aggregator.release-preprod.api.mithril.network/aggregator
export GENESIS_VERIFICATION_KEY=5b3132372c37332c3132342c3136312c362c3133372c3133312c3231332c3230372c3131372c3139382c38352c3137362c3139392c3136322c3234312c36382c3132332c3131392c3134352c31332c3233322c3234332c34392c3232392c322c3234392c3230352c3230352c33392c3233352c34345d
digest=$(mithril-client cdb snapshot list --json | jq -r .[0].digest)
(cd "${NODE_DB}" && mithril-client cdb download "$digest" && mv db preprod)

Get a usable cardano-deposit-wallet package

To use the following instructions you will need to set PACKAGED_FOR to the platform you are using:

export PACKAGED_FOR=linux64

export PACKAGED_FOR=macos-silicon

export PACKAGED_FOR=macos-intel

ATM the invocation for the deposit wallet differs between released package and the unreleased one. The released package is invoked with cardano-deposit and the unreleased one is invoked with cardano-deposit-wallet. To be fixed after release

Now you can choose to download the latest version of the cardano-deposit-wallet tarball or use a local package or build the package locally.

Download the latest version of the cardano-deposit-wallet tarball or use a

local package

COMMAND="cardano-wallet"
SHELLEY_WALLET_PORT=$(shuf -i 1024-65000 -n 1)
LEGACY_PORT="--port $SHELLEY_WALLET_PORT"
WALLET_VERSION=$(curl -s https://api.github.com/repos/cardano-foundation/cardano-deposit-wallet/releases/latest | jq -r .tag_name)
WALLET_PACKAGE=cardano-deposit-wallet-$WALLET_VERSION-$PACKAGED_FOR.tar.gz
wget -q https://github.com/cardano-foundation/cardano-deposit-wallet/releases/download/$WALLET_VERSION/$WALLET_PACKAGE
export WALLET_PACKAGE

Alternatively

Build the package locally

Set the FLAKE variable if you are working on a local clone, or leave it as it is to use the GitHub repository directly at main branch.

To compile different branches directly from the repository, you can set REF to the branch name. To compile different commits directly from the repository, you can set REV to the commit hash.

You may want to override the SYSTEM variable if you are compiling for different processor architectures on macOS.

SYSTEM can be set to x86_64-darwin, or aarch64-darwin. If not set it will default to the current system.

COMMAND="cardano-deposit-wallet"
LEGACY_PORT=""
REPOSITORY="github:cardano-foundation/cardano-deposit-wallet"
if [ -z "${FLAKE:-}" ]; then
    if [ -n "${REF:-}" ]; then
        FLAKE="$REPOSITORY/$REF"
    elif [ -n "${REV:-}" ]; then
        FLAKE="$REPOSITORY/$REV"
    else
        FLAKE="$REPOSITORY"
    fi
fi
if [ -z "${SYSTEM:-}" ]; then
    SYSTEM_FLAG=""
else
    SYSTEM_FLAG="--system $SYSTEM"
fi
VERSION=$(nix eval --raw $FLAKE#version)
export WALLET_PACKAGE="result/cardano-deposit-wallet-$VERSION-$PACKAGED_FOR.tar.gz"
nix build $SYSTEM_FLAG $FLAKE#$PACKAGED_FOR.package

Unpack the wallet package

Once the WALLET_PACKAGE is set, you can unpack it.

tar xvzf "$WALLET_PACKAGE" > /dev/null
WALLET_DIR=$(pwd)
export WALLET_DIR
export PATH=$WALLET_DIR:$PATH

Node database initialization

It is recommended to retrieve the node state from Mithril to avoid long waiting times.

Mithril node database setup

Manage processes

We are going to use screen to keep the processes running in the background, but you can use any other tool you prefer.

If you are using these instructions as a script, you should install cleanups to ensure the screen sessions are closed.

Otherwise, you can skip the next step and clean up the screen sessions manually at the end.

cleanup() {
    screen -S "$NODE_SESSION" -X quit || true
    screen -S "$WALLET_SESSION" -X quit || true
}
trap cleanup EXIT
trap cleanup SIGINT

Start the node

Now you can start the node that comes bundled with the wallet:

NODE_SESSION="node-session-$(shuf -i 1000000-9999999 -n 1)"
NODE_CONFIGS="$WALLET_DIR/configs/preprod"
export NODE_CONFIGS
screen -dmS "$NODE_SESSION" cardano-node run \
    --config "$NODE_CONFIGS/config.json" \
    --database-path "$NODE_DB/preprod" \
    --socket-path "$NODE_DB/preprod/node.socket" \
    --topology "$NODE_CONFIGS/topology.json"

You can observe the node logs with:

screen -r "$NODE_SESSION"

Detach from the screen with Ctrl-a d.

Start the wallet

Now you can start the wallet:

WALLET_SESSION="wallet-session-$(shuf -i 1000000-9999999 -n 1)"
DEPOSIT_PORT=$(shuf -i 1024-65000 -n 1)
export DEPOSIT_PORT
screen -dmS "$WALLET_SESSION" "$COMMAND" serve \
    --node-socket "$NODE_DB/preprod/node.socket" \
    --testnet "$NODE_CONFIGS/byron-genesis.json" \
    --ui-deposit-port "$DEPOSIT_PORT" $LEGACY_PORT

At the moment, the legacy port is required even if we are not using it. Once the deposit wallet is extracted from the shelley wallet code-base, the legacy port will be removed.

You can observe the wallet logs with:

screen -r "$WALLET_SESSION"

Detach from the screen with Ctrl-a d.

Test the web UI

Use curl to check if the UI is up

sleep 15
curl -s "http://localhost:$DEPOSIT_PORT" > /dev/null

Open the web UI with your browser

Now you can connect to the web UI with:

xdg-open "http://localhost:$DEPOSIT_PORT"

Cleanup screen sessions

Clean up the screen sessions using:

screen -S "$NODE_SESSION" -X quit
screen -S "$WALLET_SESSION" -X quit

You can use 2 different methods to run the cardano-deposit-wallet in a docker container.

1. Use the latest release image from docker-hub as described
2. Build the docker image locally from a commit on the repository as described

Once you have the image you will need to download the docker-compose and setup the environment.

After that you can start the service and check that the wallet is working or use the web UI. Instructions here are machine checked and so contains some bash code to execute clean-ups which are not necessary for manual execution.

Use the latest release image from docker-hub

Get latest docker-image released

tag=$(curl -s https://api.github.com/repos/cardano-foundation/cardano-deposit-wallet/releases/latest | jq -r '.tag_name')
export WALLET_TAG=$tag

Pull the docker image

docker pull cardanofoundation/cardano-deposit-wallet:$tag

Or, alternatively you can build the docker image locally.

Build the docker image locally from a commit on the repository

You will need a working nix environment to build the docker image. More information on how to install nix can be found here. A solution that runs nix in a docker container will come soon.

Select the flake version

To compile different commits directly from the repository, you can set REV to the commit hash.

REPOSITORY="github:cardano-foundation/cardano-deposit-wallet"

if [ -z "${REV:-}" ]; then
    DEFAULT_FLAKE_URL="$REPOSITORY?REF=main"
else
    DEFAULT_FLAKE_URL="$REPOSITORY?rev=$REV"
fi

FLAKE=${FLAKE:-$DEFAULT_FLAKE_URL}

if [ -z "${SYSTEM:-}" ]; then
    SYSTEM_FLAG=""
else
    SYSTEM_FLAG="--system $SYSTEM"
fi
VERSION=$(nix eval --raw $FLAKE#version)

Build the docker image

image="cardano-deposit-wallet-$VERSION-docker.tar.gz"

nix build $FLAKE#docker-image --out-link "result/$image"

Load the docker image

docker load -i "result/$image"
export WALLET_TAG=$VERSION

Download the docker-compose file

curl -s -o docker-compose.yml https://raw.githubusercontent.com/cardano-foundation/cardano-deposit-wallet/$WALLET_TAG/run/docker/docker-compose.yml

Setup the environment

Because the docker-compose.yaml is parameterized, you will need to set the environment variables before starting the service. You will need to have the variables set in the environment to run any docker compose command.

export NETWORK=preprod
export USE_LOCAL_IMAGE=true
export DEPOSIT_WALLET_UI_PORT=${DEPOSIT_WALLET_UI_PORT:-4164}
export WALLET_PORT=${WALLET_PORT:-40036}
export NODE_SOCKET_DIR=${NODE_SOCKET_DIR:-.}
export NODE_DB=${NODE_DB:-./node-db}
export WALLET_DB=${WALLET_DB:-./wallet-db}
export NODE_SOCKET_NAME=${NODE_SOCKET_NAME:-node.socket}
export USER_ID=$(id -u)
export GROUP_ID=$(id -g)

Create the directories

mkdir -p $WALLET_DB
rm -rf $WALLET_DB/*
mkdir -p $NODE_DB
rm -rf $NODE_DB/*

Auto cleanup

In case you are using this instruction as a test script you want to set up the cleanup of the environment otherwise you can skip this step.

cleanup() {
    docker compose down || true
    rm -rf $WALLET_DB
    rm -rf $NODE_DB
    rm -f docker-compose.yml
}
trap cleanup EXIT

Mithril node state preload (optional)

It's critical that we target the right network with the variables. In this case, we are targeting the preprod network. See Mitrhil documentation for more information.

export AGGREGATOR_ENDPOINT=https://aggregator.release-preprod.api.mithril.network/aggregator
export GENESIS_VERIFICATION_KEY=5b3132372c37332c3132342c3136312c362c3133372c3133312c3231332c3230372c3131372c3139382c38352c3137362c3139392c3136322c3234312c36382c3132332c3131392c3134352c31332c3233322c3234332c34392c3232392c322c3234392c3230352c3230352c33392c3233352c34345d
export MITHRIL_TAG=2450.0-c6c7eba
digest=$(docker compose --profile mithril run --rm mithril cdb snapshot list --json | jq -r .[0].digest)
docker compose --profile mithril run --rm mithril cdb download "$digest"

Start the service

docker compose up -d

Check the wallet is working

sleep 10 # give some time for the containers to start
if ! curl -s http://localhost:$DEPOSIT_WALLET_UI_PORT | grep -q "Deposit Cardano Wallet";
then
    echo "Deposit Wallet is not running"
    exit 1
fi

Open wallet UI

Instructions on the web-UI can be found here.

xdg-open http://localhost:$DEPOSIT_WALLET_UI_PORT

Inspect the logs

docker compose logs -f

Stop the containers

docker compose down

Manual cleanup

rm -rf $WALLET_DB
rm -rf $NODE_DB
rm -f docker-compose.yml

TODO

TODO

API is not yet active.

Problem: Origin of incoming payments

The main goal of the Cardano Deposit Wallet is to offer a solution for the following problem:

Problem statement

Some wallet users, typically businesses, would like to identify the origin of incoming payments, typically from their customers.

Status Quo

Solution: Assign one address to one customer

The most commonly used solution to tracking the origin of incoming payments is the following:

• The customer creates an account with the business.

• The business generates a unique address and associates it with this customer account.

• Any incoming payment on that address is treated as originating from that customer.

The Cardano Deposit Wallet implements this solution.

The cardano-wallet software lacks explicit support for this solution, but it is still often used for this purpose. See below.

User: Centralized Cryptocurrency Exchanges (CEX)

Exchanges enable users to trade cryptocurrencies for both crypto and fiat currencies.

Typically, CEXes keep track of one account for each customer. A customer can deposit ADA in their account (“top up”) by sending it to a Cardano address that the Exchange has associated with and communicated to the customer.

CEXes use various wallet setups:

• Single wallet for both deposits and withdrawals.
• Two wallets: one for deposits, the other one for withdrawals.

In both cases, the wallet responsible for accepting deposits tracks the addresses at which the deposit was made.

User: Small merchants

Small online stores want to know when they receive ADA from a customer who placed an order, so that they can deliver the goods.

For example, here is a feature request for cardano-wallet:

• Feature to request additional addresses for a wallet #2921

Support in cardano-wallet

Cardano-wallet currently lacks explicit support for the type of usage described above. Specifically,

• The API documentation for Byron wallets and Shelley wallets implicitly allows funds to be moved between addresses — there is no guarantee that funds sent to a wallet address originate from outside the wallet, they could come from the wallet itself!

In practice, people use cardano-wallet to track funds incoming at particular addresses anyway, typically by inspecting the transaction history.

Besides the fundamental limitation above, using cardano-wallet in this way has additional drawbacks:

Byron-style wallets have the following drawbacks:

• Addresses that have been created and imported cannot be restored from a single seed phrase.

• The Base58 encoding used for Byron addresses tolerates less errors than Bech32, making loss of funds more likely for customers.

• Address generation relies on implementation details of Haskell’s StdGen pseudorandom number generator.

Shelley-style wallet has the following drawbacks:

• Making a transaction to generate new addresses incurs a transaction fee.

• Wallets with an address gap ≠ 20 do not comply with the BIP-44 standard for account discovery; they cannot be fully restored without knowledge of the address gap.

Alternative solutions

The problem statement could also be addressed by other means. For example:

• Transaction metadata could be augmented with identifying information about the origin of incoming payments.

• Identifying information could be added to the addresses.

Solution: Transaction metadata

In traditional banking, transaction metadata is typically used to identify the origin of an incoming payment.

Also, for some cryptocurrencies, Exchanges do a single address and distinguish users by transaction metadata. This is the case for Kraken and the Stellar Lumens blockchain.

However, the notion of “one address — one customer” appears to be established for ADA by now, probably also because current user interfaces (such as Daedalus) lack good ways to add transaction metadata.

Solution: Identity from sender addresses

One could require customers to send money from a specific address. However, that would require a feature where the user wallet is able to send from a specific address. To our knowledge, such a feature has not been implemented, and it seems to interfere with intentional anonymity of addresses.

Requirements: Deposit Wallet

Synopsis

This documents describes high-level requirements on the Cardano Deposit Wallet.

The Cardano Deposit Wallet is a full-node wallet targeting businesses that need to track the origin of incoming payments ("deposits").

Such a wallet is useful to businesses who want to match incoming payments to customers. The matching works as follows:

• The customer creates an account with the business.
• In the wallet, the business generates a unique address and associates it with this customer account.
• Any incoming payment on that address is treated as originating from that customer.

Motivation

See Problem statement.

Requirements

Synopsis

Compared to cardano-wallet, the Deposit Wallet

• Officially supports a mapping between addresses to customers.

• Improves performance when handling many addresses and large UTxO sets.

• Supports a larger number of customers (up to 2³¹ ~ 2.1 Billion) in a single wallet.

• Uses the Bech32 encoding for customer addresses, which is more resilient against spelling mistakes.

• Basic User Interface for Wallet Usability and Demonstration.

Details

Main

Known customers:

• The wallet maintains a one-to-one mapping between customers and addresses.

• Customers are represented as numerical indices starting at 0.

• The maximum number of customers is at leaset 2³¹ ~ 2.1 Billion.

• Addresses are encoded using Bech32, which is more resilient against spelling mistakes.

• Addresses are derived deterministically from a public key using BIP-32-style key derivation.

Incoming transactions:

• A deposit made at an address is treated as originating from the corresponding customer.

• We can query the wallet for a recent history of deposits made by each known customer.

Outgoing transactions:

• Outgoing funds are not distinguished by customer — once funds have gone into the wallet, they are all part of a single wallet balance.

• A transaction created by the wallet does not send funds to a known customer unless the wallet user explicitly wants that customer as payment destination.

Signatures:

• The wallet stores a public key from which customer addresses are derived deterministically.

• Optionally, the wallet stores a private key in order to sign outgoing transactions. This private key is encrypted with a passphrase.

Technical

Incoming transactions:

• Rollbacks of the blockchain are supported and do not cause an inconsistent wallet state.

• The query for the history of deposits is atomic with respect to rollbacks.

• Variant queries for the history of deposits are supported

Outgoing transactions:

• The wallet can create a valid transaction if sufficient funds are available.

• The wallet can sign the transaction if the optional private key is stored.

API:

• REST API that exposes the wallet functionality

• web UI for testing purposes

Non-Functional

Performance

• The wallet state is persisted to disk and does not need to be recreated by synchronizing to the blockchain.

• Time-complexity of reading a new block should be

  • logarithmic in the size of the address↔︎customer mapping

  • logarithmic in the size of the current wallet UTxO

Specification: Customer Deposit Wallet

This document is a COPY. The source of truth is currently located at the repository cardano-foundation/cardano-wallet-agda.

Revision 2025-02-13

Introduction

This document specifies the core functionality of a customer deposit wallet, or deposit wallet for short.

A deposit wallet's main purpose is to track the origin of incoming funds:

1. Each customer is assigned a unique address belonging to the wallet, and a deposit made at this address is treated as originating from that customer.
2. Outgoing funds are not distinguished by customer: once funds have gone into the wallet, they are all part of a single wallet balance.

A deposit wallet is useful for businesses who need to track a large number of customers, such as centralized exchanges (CEX) or e-shops on Cardano.

Motivation

On Cardano, a transaction that spends money from a wallet typically has transaction outputs that return change to the wallet. For the Deposit Wallet, it is critically important that these change outputs are not assigned to any known customer addresses — otherwise they would be treated as originating from a customer!

However, this property is not guaranteed for other wallet software, such as cardano-wallet — and this led to a very expensive bug, where customers were credited with funds that they had never deposited.

The main motivation for this specification is therefore to explicitly state that this property should hold, to formulate it with precision, and to do so in a way that is amenable to compiler-checked proof.

More precisely, we use Agda to formally define data structures and functions that allow us ultimately to state and prove the aforementioned property.

High-level Requirements

We now outline high-level requirements for the Deposit Wallet — these include generic requirements on wallet software, but also the crucial property mentioned above. The rest of this document turns these high-level requirements into actual machine-checkable code!

We require that the wallet has a notion of known customers, specifically

• Each customer is represented by a numerical index starting at 0.
• The wallet maintains a one-to-one mapping between known customers and addresses.

For incoming transactions,

• We can query the wallet for a recent history of deposits made by each known customer.

For outgoing transactions,

1. The wallet can create a transaction successfully if it has sufficients funds to cover the payments and a small amount of fees.
2. The transaction will be accepted by the Cardano ledger.
3. The transaction reflects the intention, i.e. only the desired payments are made, and all other transaction outputs belong to the wallet.
4. Last but not least, the transaction does not send funds to a known customer unless that customer is specifically mentioned as payment destination.

Setup

This document is a literate Agda file: It contains prose that describes and explains the specification, but it also contains definitions and logical properties that can be checked by the proof assistant Agda.

When implementing this specification, we intend to create a machine-checked proof that our implementation matches this specification. However, this specification only covers the core functionality of the software application to be implemented, not the full software. We proceed as follows:

• The full software application will be implemented in Haskell. Sizeable parts of the functionality will be tested, not proven.

• However, the core functionality that is covered by this specification will be implemented using Agda and exported to Haskell via the agda2hs transpiler. This core functionality will be proven, not tested.

• In turn, proofs about the core functionality will depend on the assumption that more basic data types provided by Haskell libraries, such as the Data.Set type, have implementations that match a specification. For the time being, we accept that this is an assumption and that the library implementations have only been tested. We postulate specifications in Agda as far as needed.

module Specification where

Imports

In order to formulate the specification, we need to import standard Haskell vocabulary

open import Haskell.Prelude
open import Haskell.Reasoning

and also

• Specification.Common — Minor additional Haskell concepts.

In addition, we also need to import concepts that are specific to Cardano:

• Specification.Cardano
  • Specification.Cardano.Chain — Types ChainPoint, Slot.
  • Specification.Cardano.Tx — Transaction type Tx.
  • Specification.Cardano.Value — Monetary Value. Includes both native coins (ADA) and user-defined assets, such as stablecoins or NFTs.

Specification

Overview

This specification of a customer deposit wallet amounts to the specification of an abstract data type WalletState, which represents the entire state of such a wallet.

The goal of this document is to specify the operations on this abstract data type and the logical properties that relate them.

We define a module DepositWallet which is parametrized by

• the abstract data type WalletState that we wish to specify,
• a specification SigCardano of Cardano-related concepts that we need to formulate this specification, and
• a specification SigWallet of wallet-related concepts that are not the focus of this document.

module
  DepositWallet
    (WalletState : Set)
    (XPub : Set)
    (SigCardano : Specification.Cardano.Signature)
    (SigWallet  : Specification.Wallet.UTxO.Signature SigCardano)
  where

  open Specification.Cardano.Signature SigCardano
  open Specification.Wallet.UTxO.Signature SigWallet

Operations

We now list all auxiliary data types and all operations supported by the abstract data type WalletState. This list is meant for reference — we will explain each of them in detail in the subsequent sections.

Auxiliary data types:

  Customer = Word31

  record ValueTransfer : Set where
    field
      spent    : Value
      received : Value

  open ValueTransfer

  TxSummary : Set
  TxSummary = Slot × TxId × ValueTransfer

Operations:

  record Operations : Set where
    field

      deriveCustomerAddress : XPub → Customer → Address
      fromXPubAndCount      : XPub → Word31 → WalletState
      listCustomers         : WalletState → List (Customer × Address)

      applyTx       : ChainPoint → Tx → WalletState → WalletState
      getWalletSlot : WalletState → Slot
      totalUTxO     : WalletState → UTxO
      isOurs        : WalletState → Address → Bool

      getCustomerHistory
        : WalletState → Customer → List TxSummary

      createPayment
        : List (Address × Value)
        → PParams → WalletState → Maybe TxBody

Properties

In subsequent sections, we will specify the properties that the operations should satisfy.

The following record collects the properties:

  record Properties (O : Operations) : Set₁ where
    open Operations O

Mapping between Customers and Addresses

The defining feature of the deposit wallet is that it keeps track of a mapping between customers and addresses. We begin by specifying this mapping.

The type Customer denotes a unique identifier for a customer. For reasons explained later, we choose to represent this type as a numerical index:

Customer = Word31

The mapping between customers and addresses is maintained by the following operations:

deriveCustomerAddress : XPub → Customer → Address

fromXPubAndCount      : XPub → Word31 → WalletState
listCustomers         : WalletState → List (Customer × Address)

Here,

• deriveCustomerAddress deterministically creates an address for a given customer index.

• fromXPubAndCount xpub count creates an empty WalletState at genesis which keeps track of count many customers, starting at index 0. Their addresses are derived deterministically from the public key xpub.

• listCustomers returns the mapping between customers and addresses currently maintained by the WalletState.

In order to make the specification clear and simple, we do not allow the mapping between customers and addresses to change after creation — the idea is that listCustomers will always return the same result, no matter how the WalletState is changed subsequently.

The result of the function listCustomers contains the entire mapping between customers and addresses. The following definitions make this mapping easier to discuss:

    customerAddress : Customer → WalletState → Maybe Address
    customerAddress c = lookup c ∘ listCustomers

    knownCustomer : Customer → WalletState → Bool
    knownCustomer c = isJust ∘ customerAddress c

    knownCustomerAddress : Address → WalletState → Bool
    knownCustomerAddress a = elem a ∘ map snd ∘ listCustomers

We require that the mapping is a bijection

    unique : {{Eq a}} → List a → Bool
    unique xs = nub xs == xs

    isBijection : ∀ {{_ : Eq a}} {{_ : Eq b}} → List (a × b) → Bool
    isBijection xys = unique (map fst xys) && unique (map snd xys)

    field
      prop-listCustomers-isBijection
        : ∀ (w : WalletState)
        → isBijection (listCustomers w) ≡ True

The relation between listCustomers and fromXPubAndCount is specified as follows: First, the mapping precisely contains count many customers, starting at index 0:

      prop-listCustomers-fromXPubAndCount-range
        : ∀ (c : Customer) (xpub : XPub) (count : Word31)
        → knownCustomer c (fromXPubAndCount xpub count)
          ≡ (0 <= c && c < count)

Second, the addresses are derived deterministically from the public key and the customer index.

      prop-listCustomers-fromXPubAndCount-xpub
        : ∀ (c     : Customer)
            (xpub  : XPub)
            (count : Word31)
            (addr  : Address)
        → customerAddress c (fromXPubAndCount xpub count)
          ≡ Just addr
        → deriveCustomerAddress xpub c
          ≡ addr

The idea is that these properties hold not only for the initial state at fromXPubAndCount, but also for any state obtained through other operations such as applyTx.

For compatibility with hardware wallets and the BIP-32 standard, we derive the Address of each customer from the root private key of the wallet in a deterministic fashion. Specifically, using the notation of BIP-32 in pseudo-code, we require that

deriveCustomerAddress : WalletState → Word31 → Address
  deriveCustomerAddress s ix = rootXPrv s / 1857' / 1815' / 0' / 0 / ix

Here, 1857 is a new “purpose” identifier; we cannot reuse the CIP-1852 standard, because it behaves differently when discovering funds in blocks.

This method of deriving addresses is also the reason why we choose a concrete representation of Customer as Word31.

Transactions and slots

Transactions are used to spend from or send funds to a wallet. The type Tx represents a transaction. The WalletState may keep a history of transactions. In order to keep a history, we need a notion of time — we use the type Slot to keep track of time, as this type represents a time interval in which one block can be forged.

In order to apply a Tx to the WalletState, we specify a function

applyTx : ChainPoint → Tx → WalletState → WalletState

The first argument of this function is the ChainPoint that references the block in which the transaction was included. To get the Slot of this block, use the function slotFromChainPoint.

Transactions have to be applied in increasing Slot order. For this reason, we also specify a function

getWalletSlot : WalletState → Slot

that records the last Slot for which a transaction was applied; we express this property as:

      prop-getWalletSlot-applyTx
        : ∀ (w     : WalletState)
            (point : ChainPoint)
            (tx    : Tx)
        → let slot = slotFromChainPoint point
          in  (getWalletSlot w <= slot) ≡ True
              → getWalletSlot (applyTx point tx w)
                ≡ slot

An initial WalletState created with fromXPubAndCount starts at genesis:

      prop-getWalletSlot-fromXPubAndCount
        : ∀ (xpub  : XPub)
            (count : Word31)
        → getWalletSlot (fromXPubAndCount xpub count)
          ≡ genesis

For completeness, we decree that applyTx with a past Slot are a no-op on the WalletState:

      prop-getWalletSlot-applyTx-past
        : ∀ (w     : WalletState)
            (point : ChainPoint)
            (tx    : Tx)
        → (getWalletSlot w <= slotFromChainPoint point) ≡ False
        → applyTx point tx w
          ≡ w

Finally, we specify that the mapping between customers and addresses is unchanged by transactions:

      prop-listCustomers-applyTx
        : ∀ (w     : WalletState)
            (point : ChainPoint)
            (tx    : Tx)
        → listCustomers (applyTx point tx w)
            ≡ listCustomers w

Wallet balance and transactions

The primary purpose of a wallet is to keep track of funds that are available for spending.

On the Cardano blockchain, this means keeping track of unspent transaction outputs (UTxO). This topic is discussed in more detail in

• Specification.Wallet.UTxO

Here, we only introduce basic concepts of UTxO management, as we want to focus on the relation between customer addresses and funds in the wallet.

The basics of UTxO management are as follows: The total UTxO of the wallet that can be spent is given by the function

totalUTxO : WalletState → UTxO

A transaction of type Tx may spend some outputs and create new ones. We assume that a function

applyTxToUTxO : (Address → Bool) → Tx → UTxO → UTxO

applies the transaction to the UTxO. Here, the first argument is a predicate that specifies which output addresses of a transactions belong to the wallet. For the Deposit Wallet, the addresses belonging to the wallet are given by a function

isOurs : WalletState → Address → Bool

Now, we extend the discussion to the entire WalletState: First, we consider the predicate isOurs. We require that all known customer addresses belong to the wallet

      prop-knownCustomerAddress-isOurs
        : ∀ (addr : Address)
            (w    : WalletState)
        → knownCustomerAddress addr w ≡ True
        → isOurs w addr ≡ True

However, there may be additional addresses belonging to the wallet, in particular change addresses.

Second, we consider the application of a transaction. We require that applyTx is equivalent to applyTxToUTxO on the totalUTxO:

      prop-totalUTxO-applyTx
        : ∀ (point : ChainPoint)
            (tx    : Tx)
            (w     : WalletState)
        → (getWalletSlot w <= slotFromChainPoint point) ≡ True
        → totalUTxO (applyTx point tx w)
            ≡ applyTxToUTxO (isOurs w) tx (totalUTxO w)

Tracking incoming funds

The wallet tracks all addresses in listCustomers whenever new blocks are incorporated into the wallet state.

The result of tracking is given by the operation

getCustomerHistory : WalletState → Customer → List TxSummary

For a given customer, this operation returns a list of transaction summaries. A transaction summary (TxSummary) reports the total Value spent or received by the customer within a specific transaction. The summary also includes the transaction id (TxId) and the Slot at which the transaction was included in the blockchain.

record ValueTransfer : Set where
  field
    spent    : Value
    received : Value

open ValueTransfer

TxSummary : Set
TxSummary = Slot × TxId × ValueTransfer

Note that the deposit wallet does not support delegation and reward accounts — the spent field only records value spent from transaction outputs.

The main purpose of the function getCustomerHistory is to track the origin of incoming funds. When a transactions makes a payment to an address that belongs to a known customer c, customerAddress c ≡ Just address, a transaction summary with the corresponding transaction id will show up in the result of getCustomerHistory for the customer c. This summary will record the total value that this customer received in this transaction.

Note that the spent field in the TxSummary is for information only — the deposit wallet does not distinguish customers when spending, funds are taken out from customer addresses at random. See the discussion of createPayment in a later section.

In order to specify the behavior of getCustomerHistory more precisely, we assume two functions

spentTx    : Address → Tx → UTxO → Value
receivedTx : Address → Tx → Value

which total the value spend, respectively received, at a given address when a transaction is applied to a UTxO. These functions are from Specification.Wallet.UTxO. We group them in a function

    summarizeTx : Address → Tx → UTxO → ValueTransfer
    summarizeTx addr tx u = record
      { spent    = spentTx addr tx u
      ; received = receivedTx addr tx
      }

Now, we require that applying a transaction to the wallet state will add the summary of this transaction to getCustomerHistory:

    field
      prop-getCustomerHistory-applyTx
        : ∀ (c       : Customer)
            (address : Address)
            (point   : ChainPoint)
            (tx      : Tx)
            (w       : WalletState)
        → (c , address) ∈ listCustomers w
        → let slot = slotFromChainPoint point
          in  (getWalletSlot w <= slot) ≡ True
            → getCustomerHistory (applyTx point tx w) c
              ≡ (slot , getTxId tx , summarizeTx address tx (totalUTxO w))
                ∷ getCustomerHistory w c

On the other hand, customers that are not known will not be tracked:

      prop-getCustomerHistory-knownCustomer
        : ∀ (w : WalletState)
            (c : Customer)
        → knownCustomer c w ≡ False
        → getCustomerHistory w c
          ≡ []

Finally, a wallet that was just initialized does not contain a history of transactions, yet:

      prop-getCustomerHistory-fromXPubAndCount
        : ∀ (xpub : XPub)
            (count : Word31)
            (c : Customer)
        → getCustomerHistory (fromXPubAndCount xpub count) c
          ≡ []

The above properties provide a specification of tracking incoming funds via getCustomerHistory. For larger transaction histories, this function may not offer the best performance — for example, it does not limit the list of transactions, and we cannot query recent transactions by customers. However, we only specify one function here, because these other queries can be specified in terms of the result of getCustomerHistory alone, without further reference to the WalletState.

Creating transactions

The main purpose of a wallet is to keep track of funds available for spending — and to provide a method for spending them when desired. For the latter task, we specify an operation

createPayment
  : List (Address × Value)
  → PParams → WalletState → Maybe TxBody

which maybe constructs a transaction that sends given Values to given destination Addresses. Here, PParams are protocol parameters such as maximum transaction size or fee size that are needed to construct a valid transaction.

In the beginning of this document, we have stated four high-level requirements that transactions created by the deposit wallet should respect. However, there are also requirements that we do not impose. Specifically, we do not require that createPayment picks any particular transaction inputs — all funds within the wallet are treated as interchangeable, and can be spent as desired. In other words, we do not distinguish funds in the wallet by customer anymore — we only track the customer when funds move into the wallet. This is in contrast to alternative wallet styles that track a per-customer balance.

Formalizing the high-level requirements for outgoing transactions is laborious. The first requirement is difficult to implement, we defer its discussion to Specification.Wallet.Payment. The second requirement would need a more detailed formalization of the Cardano ledger UTXO and UTXOW rules, which is out of scope here.

Fortunately, not meeting the first two requirements only makes the software less useable, as this would only mean that we cannot create some desired transactions — but we never create transactions that go against our intentions. Hence, we only formalize the third and fourth requirement here.

We formalize the third requirement in two properties:

• Each payment destination has to appear at least once in the transaction outputs.
• Conversely, each transaction output has to be a payment output or has to belong to the wallet.

We formalize the first property as follows: Assuming that createPayment applied to the payment destinations succeeds, we require that the destinations are a subsequence of the transactions outputs:

    field
      prop-createPayment-destinations
        : ∀ (w  : WalletState)
            (pp : PParams)
            (destinations : List (Address × Value))
            (tx : TxBody)
          → createPayment destinations pp w ≡ Just tx
          → isSubsequenceOf destinations (outputs tx)
            ≡ True

Above, we have to be mindful of the possibility that payments destinations can be duplicated, that is why we use isSubsequenceOf to make sure that every one of them is included. Strictly speaking, this is unnecessarily restrictive on the order of the transaction outputs, but the order can always be arranged.

We formalize the converse property as follows:

      prop-createPayment-isOurs
        : ∀ (w  : WalletState)
            (pp : PParams)
            (destinations : List (Address × Value))
            (tx : TxBody)
          → createPayment destinations pp w ≡ Just tx
          → all (isOurs w ∘ fst) (outputs tx \\ destinations)
            ≡ True

This property above states that if createPayment destinations succeeds in creating a transaction tx, then after removing the destinations from the transaction outputs (using the operation (\\) from Data.List), all output addresses belong to the wallet. Again, we have to be mindful of the possibility that the transaction outputs may contain duplicate destinations; using the (\\) operation is the most systematic way to handle that possibility.

Finally, we formalize the fourth requirement that is specific to the deposit wallet:

      prop-createPayment-not-known
        : ∀ (pp : PParams)
            (w  : WalletState)
            (destinations : List (Address × Value))
            (tx : TxBody)
        → createPayment destinations pp w ≡ Just tx
        → ∀ (address : Address)
          → knownCustomerAddress address w ≡ True
          → ¬ (address ∈ map fst destinations)
          → ¬ (address ∈ map fst (outputs tx))

This property above states that if createPayment destinations succeeds in creating a transaction tx, then for all addresses, if that address belongs to a known customer, but does not appear in the destinations, then it shall not appear in the transaction outputs either.

Specification: Cardano Types

This document provides a partial specification of types related to the Cardano blockchain, as needed by the Deposit Wallet.

module Specification.Cardano where

Imports

open import Haskell.Prelude

import Specification.Cardano.Chain as ModChain
import Specification.Cardano.Value as ModValue
import Specification.Cardano.Tx as ModTx

Signature

A signature records data types, operations, and the properties that these operations should satisfy.

record Signature : Set₁ where
  field

We introduce new types

    CompactAddr : Set
    {{iEqCompactAddr}} : Eq CompactAddr

    PParams  : Set

and re-export the existing ones from Specification.Cardano.*

  field
    SigChain : ModChain.Signature

  field
    SigValue : ModValue.Signature
  open ModValue.Signature SigValue using (Value)

  field
    SigTx    : ModTx.Signature CompactAddr Value

  open ModChain.Signature SigChain public
  open ModValue.Signature SigValue public
  open ModTx.Signature SigTx public

For improved readability, we use the synonym

  Address = CompactAddr

to refer to addresses on Cardano.

Specification: Chain

This document provides a partial specification of types related to identifying points on the blockchain, as needed by the Deposit Wallet.

module Specification.Cardano.Chain where

Imports

open import Haskell.Prelude
open import Haskell.Reasoning

Signature

A signature records data types, operations, and the properties that these operations should satisfy.

record Signature : Set₁ where
  field

The type

    Slot : Set

that represents time intervals in which one block can be forged.

The type

    ChainPoint : Set

represents a point on the blockchain, i.e. the unique hash and Slot of a block that has been forged.

The Slot type supports equality and comparison:

    instance
      iEqSlot  : Eq Slot
      iOrdSlot : Ord Slot

This comparison is a total order:

      iIsLawfulOrdSlot : IsLawfulOrd Slot {{iOrdSlot}}

The smallest Slot is called genesis, which technically does not correspond to a block, but represents the genesis parameters of the blockchain.

    genesis : Slot

    prop-genesis-<=
      : ∀ (x : Slot)
      → (_<=_ {{iOrdSlot}} genesis x) ≡ True

The ChainPoint type supports an operation

    slotFromChainPoint : ChainPoint → Slot

that retrieves the Slot of the block that is referenced by the ChainPoint.

Specification: Transactions

This document provides a partial specification of the Tx type and related types, as needed by the Deposit Wallet.

module Specification.Cardano.Tx where

A Tx represents a transaction. A transactions creates transaction outputs and spends previously created transaction outputs.

Imports

open import Haskell.Prelude
open import Haskell.Reasoning

Signature

A signature records data types, operations, and the properties that these operations should satisfy.

record Signature (Address : Set) (Value : Set) : Set₁ where
  field

We are concerned with types

    TxBody : Set
    Tx     : Set
    TxId   : Set

that support the following operations:

    outputs : TxBody → List (Address × Value)
    getTxId : Tx → TxId

Specification: Value

This document provides a partial specification of the Value type, as needed by the Deposit Wallet.

module Specification.Cardano.Value where

A Value represents monetary value. It is a collection that contains both ADA and optionally custom assets.

Imports

open import Haskell.Prelude
open import Haskell.Reasoning

Signature

A signature records data types, operations, and the properties that these operations should satisfy.

record Signature : Set₁ where
  field

We are concerned with a single type

    Value : Set

that supports the following operations:

    empty         : Value
    add           : Value → Value → Value
    largerOrEqual : Value → Value → Bool

and an equality test

    {{iEqValue}}  : Eq Value

The operation add sums up the monetary values contained in the arguments. This operation has empty as left- and right identity.

    prop-add-x-empty
      : ∀ (x : Value)
      → add x empty ≡ x
    
    prop-add-empty-x
      : ∀ (x : Value)
      → add empty x ≡ x

The operation is both associative and commutative:

    prop-add-assoc
      : ∀ (x y z : Value)
      → add (add x y) z ≡ add x (add y z)

    prop-add-sym
      : ∀ (x y : Value)
      → add x y ≡ add y x

The operation largerOrEqual x y returns True whenever the value x constains as many or strictly more assets — both ADA and custom assets — than the value y.

In particular, adding a third value will not change the relation in size:

    prop-add-monotone
      : ∀ (x y z : Value)
      → largerOrEqual (add x z) (add y z)
        ≡ largerOrEqual x y

Specification: Common concepts

This document introduces common concepts used during the specification.

module Specification.Common where

Imports

We rely on common Haskell types, such as pairs, lists, …

open import Haskell.Prelude
open import Haskell.Reasoning
open import Haskell.Data.Maybe using (isJust) public

Additions

However, we also require a few convenience concepts not covered by the imports above.

The logical combinator "if and only if"

_⇔_ : Set → Set → Set
x ⇔ y = (x → y) ⋀ (y → x)

The predicate _∈_ records whether an item is an element of a list

_∈_ : ∀ {a : Set} {{_ : Eq a}} → a → List a → Set
x ∈ xs = elem x xs ≡ True

The predicate isSubsequenceOf records whether the elements of one list are contained in the other list, in sequence.

isSubsequenceOf : ∀ {a : Set} {{_ : Eq a}} → List a → List a → Bool
isSubsequenceOf [] _ = True
isSubsequenceOf _ [] = False
isSubsequenceOf (x ∷ xs) (y ∷ ys) =
    if x == y
    then isSubsequenceOf xs ys
    else isSubsequenceOf (x ∷ xs) ys

The function nub is missing from agda2hs:

nub : {{Eq a}} → List a → List a
nub [] = []
nub (x ∷ xs) = x ∷ filter (x /=_) (nub xs)

The function delete deletes the first occurence of the item from the list.

delete : ⦃ Eq a ⦄ → a → List a → List a
delete _ []       = []
delete x (y ∷ ys) = if x == y then ys else y ∷ delete x ys

The operator _\\_ is list difference. In the result xs \\ ys, the first occurrence of each element of ys in turn (if any) has been removed from @xs.

_\\_ : ⦃ Eq a ⦄ → List a → List a → List a
_\\_ = foldl (flip delete)

Specification: Creating Payments Success

This document discusses the success conditions of a function createPayment that creates a payment by selecting transaction outputs from a UTxO.

Imports

open import Haskell.Prelude
open import Haskell.Reasoning
open import Haskell.Data.Maybe using (isJust)

import Specification.Cardano.Value

module
  Specification.Wallet.Payment
    (ValueSig : Specification.Cardano.Value.Signature)
  where

open Specification.Cardano.Value.Signature ValueSig

Signature

A signature records data types, operations, and the properties that these operations should satisfy.

record Signature : Set₁ where
  field

Besides Value, we assume several other data types and functions

    Address : Set
    PParams : Set
    Tx      : Set
    UTxO    : Set

    balance : UTxO → Value

createPayment

The main purpose of a wallet is to send and receive funds to other people.

Given a list of monetary Value and Address to send them to, the function

    createPayment
      : List (Address × Value)
      → PParams → UTxO → Maybe Tx

creates a transaction by selecting transaction outputs from the curently available UTxO of the wallet.

The main property desired of this function is that it always succeeds in creating a transaction as long as the wallet has sufficient funds.

One way of formalizing this property would be as follows: For simplicity, let us assume that there is a maximum fee which covers any transaction:

    maxFee : PParams → Value

Then, the idea is that we can always create a transaction, as long as the available UTxO exceed the value to be paid out plus the maximum fee:

  totalValue : List (Address × Value) → Value
  totalValue = foldr add empty ∘ map snd

  field
    prop-createPayment-success
      : ∀ (utxo : UTxO)
          (pp : PParams)
          (destinations : List (Address × Value))
      → largerOrEqual
          (balance utxo)
          (add (totalValue destinations) (maxFee pp))
        ≡ True
      → isJust (createPayment destinations pp utxo) ≡ True

Unfortunately however, this property cannot hold as written on Cardano. Besides this condition of insufficient funds, there are other reasons for failure:

• Wallet UTxO is poor
  • Few UTxO which are too close to minimum ADA quantity
  • UTxO with too many native assets
• Destinations are poor
  • Value does not carry minimum ADA quantity
  • Value size too large (native assets, Datum, …)
• Combination of both:
  • Too many UTxO with small ADA amount that we need to cover a large Value payment. Example: "Have 1 million x 1 ADA coins, want to send 1 x 1'000'000 ADA coin."

We currently do not know a formal property that guarantees success of createPayment, but also admits an implementation, as this requires handling the above potential failure cases.

Specification: UTxO

This document provides an entrypoint to the specification of UTxO-style accounting for cryptocurrency wallets.

This topic is discussed in-depth in

• D. Coutts and E. de Vries. Formal specification for a Cardano wallet. (2018)

In light of this prior art, the specification of the Deposit Wallet focuses on other topics; here, we just collect the most basic notions.

module Specification.Wallet.UTxO where

Imports

open import Haskell.Prelude

import Specification.Cardano

Signature

A signature records data types, operations, and the properties that these operations should satisfy.

record
  Signature
    (SigCardano : Specification.Cardano.Signature)
    : Set₁
  where
  open Specification.Cardano.Signature SigCardano
  field

We introduce new types

    UTxO : Set

and functions

    balance : UTxO → Value

    applyTxToUTxO : (Address → Bool) → Tx → UTxO → UTxO

    spentTx    : Address → Tx → UTxO → Value
    receivedTx : Address → Tx → Value

The function balance computes the total value contained in the unspent outputs.

The function applyTxToUTxO isOurs tx utxo applies the given transaction tx to the unspent transction outputs in utxo. The predicate isOurs indicates whether the address of an output belongs to the wallet, typically because the wallet owner knows the corresponding signing key. Only those outputs that satisfy isOurs are included in the updated UTxO.

The function spentTx computes the Value spent by the transaction on the given address — without accounting for received value.

In turn, the function receivedTx computes the Value received by the transaction on the given address — without accounting for spent value.

At this level of detail, we cannot formulate any properties — we would need a definition of Tx for that purpose.

Implementation: Customer Deposit Wallet

This document describes selected aspects of the current implementation of the Cardano Deposit Wallet.

We focus on aspects that are about the overall organization of the source code and cannot be learned by looking at individual files.

TODO: This document needs to become part of the source code.

Repositories

The source code for the Cardano Deposit Wallet is currently split over several repositories and packages:

• Repo cardano-wallet-agda

  • Package customer-deposit-wallet-pure

    • Specification.
    • Implementation of main pieces of functionality using Agda2hs, in a purely functional style.

  • Package customer-deposit-wallet-pure — helper library. Also exported to agda2hs.

• Repo cardano-wallet

  • Package customer-deposit-wallet — Package that assembles the pieces of functionality from customer-deposit-wallet-pure and makes them useable in imperative styles.

  • Package customer-deposit-wallet-ui — Package that presents a web UI for the Deposit Wallet.

  • Package network-layer, … — helper packages.

  • Executable cardano-wallet — currently contains both the legacy cardano-wallet and the Deposit Wallet with UI.

• Repo cardano-deposit-wallet

  • Provides releases containing the executable.

  • Documentation.

Conformance to Specification

The package customer-deposit-wallet-pure contains both the specification and and implementation of various aspects of functionality. Some of these aspects come with proofs. An experimental implementation combines the aspects and proves a few properties of the Specification.

However, the actual implementation in customer-deposit-wallet has not been proven or tested correct with respect to the Specification yet.

Module Organization

The package customer-deposit-wallet is organized into modules with the prefix Cardano.Wallet.Deposit.*.

In turn, this prefix is organized into groups of modules. These groups build on top of each other — each group wraps the previous group, moving from purely functional style to an imperative style, with more and more integration with the operating system and other interfaces.

The succession of module groups is:

1. Pure — Implementation in purely functional style: only data types and pure functions on it.
2. IO — Straightforward wrapper of the pure functions into an interface with implicit control flow (mutable state, exceptions, concurrency).
3. REST — Straightforward wrapper of IO into an API that aligns with REST principles.
4. HTTP — Straightforward wrapper of REST into an HTTP API.

The package customer-deposit-wallet-ui add the group

4'. UI — Presentation of REST as a web UI.

Roadmap: Cardano Deposit Wallet

This roadmap describes potential directions for the Cardano Deposit Wallet.

Minimium Viable Product

Production readiness:

• Separate executable: cardano-deposit-wallet.
• Persistence: The wallet state is stored on disk and does not have to be resynchronized every time that the deposit wallet process is started.
• REST API: For interacting with the wallet.

Future work, potential

• Formal methods

  • Prove the implementation correct with respect to the specification.

• Refunds

  • Create transaction that refunds any UTxO from a customer — but which the wallet does not accept (e.g. because they contain NFTs). The user has to pay the transaction fee.

• Staking?

  • Delegate wallet funds to a stake pool.

  • A transaction output can belong to the wallet but may have a delegation part that points to a stake pool.

    • Users can stake with the funds as long as possible?

    • Should we make a transaction that moves those funds to a different delegation address?

Contributing