Account Types¶
This module defines the core types introduced by CIP 159 (Account Address Enhancement).
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. Alternatively, the balance may be asserted exactly. The four
constructors correspond to the four cases in the CIP's CDDL
required_balance_interval type.
data BalanceInterval : Type where ⟦_,_⦆ : Coin → Coin → BalanceInterval ⟦_,∞⦆ : Coin → BalanceInterval ⟦0,_⦆ : Coin → BalanceInterval Exact : 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#1821}{\htmlId{1879}{\htmlClass{Bound}{\text{lb}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Account.html#1824}{\htmlId{1884}{\htmlClass{Bound}{\text{ub}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1279}{\htmlId{1887}{\htmlClass{InductiveConstructor Operator}{\text{⦆}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1891}{\htmlId{1891}{\htmlClass{InductiveConstructor}{\text{lowerBounded}}}}\, \,\htmlId{1905}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{1907}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Account.html#1908}{\htmlId{1908}{\htmlClass{Bound}{\text{lb}}}}\, \,\htmlId{1911}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Prelude.Base.html#234}{\htmlId{1913}{\htmlClass{Function}{\text{Coin}}}}\,\,\htmlId{1917}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{1923}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1908}{\htmlId{1925}{\htmlClass{Bound}{\text{lb}}}}\, \,\href{Class.HasOrder.Core.html#613}{\htmlId{1928}{\htmlClass{Field Operator}{\text{≤}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1761}{\htmlId{1930}{\htmlClass{Bound}{\text{c}}}}\, \,\htmlId{1942}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1742}{\htmlId{1944}{\htmlClass{Datatype}{\text{InBalanceInterval}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1761}{\htmlId{1962}{\htmlClass{Bound}{\text{c}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Account.html#1908}{\htmlId{1966}{\htmlClass{Bound}{\text{lb}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Account.html#1975}{\htmlId{1975}{\htmlClass{InductiveConstructor}{\text{upperBounded}}}}\, \,\htmlId{1989}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{1991}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Account.html#1992}{\htmlId{1992}{\htmlClass{Bound}{\text{ub}}}}\, \,\htmlId{1995}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Prelude.Base.html#234}{\htmlId{1997}{\htmlClass{Function}{\text{Coin}}}}\,\,\htmlId{2001}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{2007}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1761}{\htmlId{2009}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.HasOrder.Core.html#646}{\htmlId{2011}{\htmlClass{Field Operator}{\text{<}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1992}{\htmlId{2013}{\htmlClass{Bound}{\text{ub}}}}\, \,\htmlId{2026}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1742}{\htmlId{2028}{\htmlClass{Datatype}{\text{InBalanceInterval}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1761}{\htmlId{2046}{\htmlClass{Bound}{\text{c}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Account.html#1992}{\htmlId{2052}{\htmlClass{Bound}{\text{ub}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1352}{\htmlId{2055}{\htmlClass{InductiveConstructor Operator}{\text{⦆}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#2059}{\htmlId{2059}{\htmlClass{InductiveConstructor}{\text{exact}}}}\, \,\htmlId{2073}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{2075}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Account.html#2076}{\htmlId{2076}{\htmlClass{Bound}{\text{c'}}}}\, \,\htmlId{2079}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Prelude.Base.html#234}{\htmlId{2081}{\htmlClass{Function}{\text{Coin}}}}\,\,\htmlId{2085}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{2091}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1761}{\htmlId{2093}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Agda.Builtin.Equality.html#150}{\htmlId{2095}{\htmlClass{Datatype Operator}{\text{≡}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#2076}{\htmlId{2097}{\htmlClass{Bound}{\text{c'}}}}\, \,\htmlId{2110}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1742}{\htmlId{2112}{\htmlClass{Datatype}{\text{InBalanceInterval}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1761}{\htmlId{2130}{\htmlClass{Bound}{\text{c}}}}\, \,\htmlId{2132}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Account.html#1385}{\htmlId{2133}{\htmlClass{InductiveConstructor}{\text{Exact}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#2076}{\htmlId{2139}{\htmlClass{Bound}{\text{c'}}}}\,\,\htmlId{2141}{\htmlClass{Symbol}{\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