Account Types

This module defines the core types introduced by CIP 159 (Account Address Enhancement).

{-# OPTIONS --safe #-}

open import Ledger.Dijkstra.Specification.Gov.Base using (GovStructure)

module Ledger.Dijkstra.Specification.Account
  (gs : GovStructure) (open GovStructure gs) where

open import Ledger.Prelude
open import Tactic.Derive.DecEq

Direct Deposits

A DirectDeposits map records the ADA being deposited into account addresses within a single transaction. Each entry maps the stake credential of the receiving account address to a Coin amount.

DirectDeposits : Type
DirectDeposits = Credential ⇀ Coin

Balance Intervals

CIP 159 allows a transaction to assert that an account's balance falls within a given interval. The interval is half-open: [lb, ub). Either bound may be omitted, but not both. The three constructors correspond to the three cases in the CIP's CDDL required_balance_interval type.

data BalanceInterval : Type where
  ⟦_,_⦆ : Coin → Coin → BalanceInterval
  ⟦_,∞⦆ : Coin → BalanceInterval
  ⟦0,_⦆ : Coin → BalanceInterval

The InBalanceInterval Predicate

The InBalanceInterval predicate checks whether a given Coin value c falls within a BalanceInterval. (Unlike inInterval for slots, which uses closed intervals, balance intervals are half-open.)

data InBalanceInterval (c : Coin) : BalanceInterval → Type where
  bounded       : {lb ub : Coin}  → lb ≤ c → c < ub  → InBalanceInterval c $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Account.html#1703}{\htmlId{1761}{\htmlClass{Bound}{\text{lb}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Account.html#1706}{\htmlId{1766}{\htmlClass{Bound}{\text{ub}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1226}{\htmlId{1769}{\htmlClass{InductiveConstructor Operator}{\text{⦆}}}}\,
  \,\href{Ledger.Dijkstra.Specification.Account.html#1773}{\htmlId{1773}{\htmlClass{InductiveConstructor}{\text{lowerBounded}}}}\,  \,\htmlId{1787}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{1789}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Account.html#1790}{\htmlId{1790}{\htmlClass{Bound}{\text{lb}}}}\, \,\htmlId{1793}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Prelude.Base.html#234}{\htmlId{1795}{\htmlClass{Function}{\text{Coin}}}}\,\,\htmlId{1799}{\htmlClass{Symbol}{\text{}}}}\,     \,\htmlId{1805}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1790}{\htmlId{1807}{\htmlClass{Bound}{\text{lb}}}}\, \,\href{Class.HasOrder.Core.html#613}{\htmlId{1810}{\htmlClass{Field Operator}{\text{≤}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1643}{\htmlId{1812}{\htmlClass{Bound}{\text{c}}}}\,           \,\htmlId{1824}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1624}{\htmlId{1826}{\htmlClass{Datatype}{\text{InBalanceInterval}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1643}{\htmlId{1844}{\htmlClass{Bound}{\text{c}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Account.html#1790}{\htmlId{1848}{\htmlClass{Bound}{\text{lb}}}}\, \\
  \,\href{Ledger.Dijkstra.Specification.Account.html#1857}{\htmlId{1857}{\htmlClass{InductiveConstructor}{\text{upperBounded}}}}\,  \,\htmlId{1871}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{1873}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Account.html#1874}{\htmlId{1874}{\htmlClass{Bound}{\text{ub}}}}\, \,\htmlId{1877}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Prelude.Base.html#234}{\htmlId{1879}{\htmlClass{Function}{\text{Coin}}}}\,\,\htmlId{1883}{\htmlClass{Symbol}{\text{}}}}\,     \,\htmlId{1889}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1643}{\htmlId{1891}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.HasOrder.Core.html#646}{\htmlId{1893}{\htmlClass{Field Operator}{\text{<}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1874}{\htmlId{1895}{\htmlClass{Bound}{\text{ub}}}}\,           \,\htmlId{1908}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1624}{\htmlId{1910}{\htmlClass{Datatype}{\text{InBalanceInterval}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1643}{\htmlId{1928}{\htmlClass{Bound}{\text{c}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Account.html#1874}{\htmlId{1934}{\htmlClass{Bound}{\text{ub}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1299}{\htmlId{1937}{\htmlClass{InductiveConstructor Operator}{\text{⦆}}}}\,

Note that in the upperBounded case, c is not only upper-bounded (by ub), but also lower-bounded (by 0); thus lowerBounded is the only truly "half-open" case.

Account Balance Intervals

An AccountBalanceIntervals map records the balance-interval assertions that a transaction makes, one per account credential.

AccountBalanceIntervals : Type
AccountBalanceIntervals = Credential ⇀ BalanceInterval