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 = RewardAddress ⇀ 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#1738}{\htmlId{1796}{\htmlClass{Bound}{\text{lb}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Account.html#1741}{\htmlId{1801}{\htmlClass{Bound}{\text{ub}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1229}{\htmlId{1804}{\htmlClass{InductiveConstructor Operator}{\text{⦆}}}}\,
  \,\href{Ledger.Dijkstra.Specification.Account.html#1808}{\htmlId{1808}{\htmlClass{InductiveConstructor}{\text{lowerBounded}}}}\,  \,\htmlId{1822}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{1824}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Account.html#1825}{\htmlId{1825}{\htmlClass{Bound}{\text{lb}}}}\, \,\htmlId{1828}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Prelude.Base.html#234}{\htmlId{1830}{\htmlClass{Function}{\text{Coin}}}}\,\,\htmlId{1834}{\htmlClass{Symbol}{\text{}}}}\,     \,\htmlId{1840}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1825}{\htmlId{1842}{\htmlClass{Bound}{\text{lb}}}}\, \,\href{Class.HasOrder.Core.html#613}{\htmlId{1845}{\htmlClass{Field Operator}{\text{≤}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1678}{\htmlId{1847}{\htmlClass{Bound}{\text{c}}}}\,           \,\htmlId{1859}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1659}{\htmlId{1861}{\htmlClass{Datatype}{\text{InBalanceInterval}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1678}{\htmlId{1879}{\htmlClass{Bound}{\text{c}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Account.html#1825}{\htmlId{1883}{\htmlClass{Bound}{\text{lb}}}}\, \\
  \,\href{Ledger.Dijkstra.Specification.Account.html#1892}{\htmlId{1892}{\htmlClass{InductiveConstructor}{\text{upperBounded}}}}\,  \,\htmlId{1906}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{1908}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Account.html#1909}{\htmlId{1909}{\htmlClass{Bound}{\text{ub}}}}\, \,\htmlId{1912}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Prelude.Base.html#234}{\htmlId{1914}{\htmlClass{Function}{\text{Coin}}}}\,\,\htmlId{1918}{\htmlClass{Symbol}{\text{}}}}\,     \,\htmlId{1924}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1678}{\htmlId{1926}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.HasOrder.Core.html#646}{\htmlId{1928}{\htmlClass{Field Operator}{\text{<}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1909}{\htmlId{1930}{\htmlClass{Bound}{\text{ub}}}}\,           \,\htmlId{1943}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1659}{\htmlId{1945}{\htmlClass{Datatype}{\text{InBalanceInterval}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1678}{\htmlId{1963}{\htmlClass{Bound}{\text{c}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Account.html#1909}{\htmlId{1969}{\htmlClass{Bound}{\text{ub}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1302}{\htmlId{1972}{\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