16.1 Predica data model for CATS

Predica can be used to give the CATS data model a precise, machine-readable form. The model below separates enduring entities, such as Persons, accounts and loans, from the append-only events that change their derived state. It is intended to state the essential data and invariants independently of database tables, network messages and the distribution of Persons among CATS nodes.

Simple closed classifications are represented by enumerated types. A positive quantity is given its own subtype so that declarations which use it do not have to repeat the condition that an amount is greater than zero.


type PositiveInteger = subtype Integer where this > 0;
type Timestamp = subtype Integer where this ≥ 0;

enum AccountRole
{
    property,
    claim,
    liability
}

entity Node
{
    Integer id;
    key {id};
}

entity Person
{
    Integer id;
    Node node;
    key {id};
}

Every Person is assigned to one node. This allows all changes to the accounts of one Person to be committed by a local database transaction. It does not imply that the node owns the Person's accounts or anything recorded in them.

Account units and accounts

An account unit is a variant because the alternatives carry different information. A Rune needs no additional description, a foreign currency has a denomination, a fungible commodity has a defined measurement unit and grade, a Product account identifies a Product category, and an account for an identified item refers to that particular item. The variant is closed at the broad representational level, while entities such as ProductCategory and FungibleUnit allow new kinds of property to be registered without changing the variant declaration.


entity CurrencyUnit
{
    String code;
    String name;
    key {code};
}

entity FungibleUnit
{
    Integer id;
    String name;
    String measurementUnit;
    String grade;
    key {id};
}

entity ProductCategory
{
    Integer id;
    String description;
    key {id};
}

entity IdentifiedItem
{
    Integer id;
    ProductCategory category;
    String identifier;
    key {id};
    key {category, identifier};
}

variant AccountUnit
{
    {} rune;
    CurrencyUnit foreignCurrency;
    FungibleUnit fungible;
    ProductCategory product;
    IdentifiedItem identifiedItem;
}

entity Account
{
    Integer id;
    Person owner;
    AccountRole role;
    AccountUnit unit;
    key {id};
}

The owner, role and unit are part of the identity and permanent interpretation of an account. They do not change. A change of ownership is represented by a transfer between accounts, not by changing the owner attribute. An account whose unit is an identified item can only have a derived balance of zero or one; accounts for fungible units may have any non-negative integer balance.

Transactions, entries and balances

CATS uses an append-only transaction history. Each committed transaction contains one or more account entries. An entry says that an account was debited or credited by a positive amount. It does not store a replacement balance.


enum EntryDirection
{
    debit,
    credit
}

entity Transaction
{
    Integer id;
    Timestamp committedAt;
    AccountEntry entry+ where entry.transaction = this;
    key {id};
}

entity AccountEntry
{
    Integer id;
    Transaction transaction;
    Account account;
    EntryDirection direction;
    PositiveInteger amount;
    key {id};
}

The current balance is a derived value. Conceptually, for an account \(a\), it is

\[ b(a)= \sum_{e:\,e.account=a\,\wedge\,e.direction=\mathrm{credit}}e.amount - \sum_{e:\,e.account=a\,\wedge\,e.direction=\mathrm{debit}}e.amount. \]

The CATS constraint is \(b(a)\geq 0\) for every account. A node must test this derived post-transaction balance before committing a transaction. Consequently, a later entry cannot spend the same units again merely because another node has not yet received notification of the earlier transaction.

An account transfer has exactly one debit entry and one credit entry. Its constraints state the compatibility rule directly.


entity AccountTransfer
{
    Integer id;
    Transaction debitTransaction;
    Transaction creditTransaction;
    AccountEntry debitEntry;
    AccountEntry creditEntry;
    key {id};

    constraints
    {
        debitEntry.transaction = debitTransaction;
        creditEntry.transaction = creditTransaction;
        debitEntry.direction = debit;
        creditEntry.direction = credit;
        debitEntry.amount = creditEntry.amount;
        debitEntry.account.role = creditEntry.account.role;
        debitEntry.account.unit = creditEntry.account.unit;
    }
}

A transaction may contain several transfers and other operations. For example, an escrow release may transfer Runes, transfer ownership of a Product, and create a product loan. Those operations refer to the same transaction or to linked local transactions and proofs; an AccountTransfer is only the primitive movement between two compatible accounts.

Loans

A loan is an enduring entity whose quantities are recorded in associated Claim and Liability accounts. It begins with a matched Claim/Liability pair, but a partial transfer can distribute its outstanding quantity among several compatible accounts. The owners of Claim accounts holding part of the loan are its lenders for those quantities; the owners of the corresponding Liability accounts are its borrowers. This definition uses loan, lender and borrower in the general CATS sense: the property owed need not be money and the loan may arise from a purchase awaiting delivery.


entity Contract
{
    Integer id;
    String permanentReference;
    String digest;
    key {id};
    key {permanentReference};
}

entity Loan
{
    Integer id;
    AccountUnit unit;
    Contract terms;
    key {id};
}

entity LoanEntry
{
    Loan loan;
    AccountEntry entry;
    key {entry};

    constraints
    {
        entry.account.unit = loan.unit;
        (entry.account.role = claim) ∨ (entry.account.role = liability);
    }
}

The LoanEntry relation identifies the loan to which each Claim or Liability entry belongs. It therefore says which part of an account balance belongs to a particular loan. The loan identifier and contract distinguish loans that happen to use the same unit. A claim for one hundred grams of gold from one borrower is therefore not silently merged with a claim for the same quantity from another borrower or under different terms. The current lenders and borrowers are derived from the owners of the associated accounts and the outstanding quantity allocated to each account.

Loan changes are represented by a variant. The variant makes the alternatives mutually exclusive and allows each alternative to carry exactly the data it requires. All quantities remain positive; the alternative determines whether the outstanding balance increases or decreases.


value LoanIncrease
{
    Loan loan;
    PositiveInteger amount;
    Transaction transaction+;
}

value InterestAccrual
{
    Loan loan;
    PositiveInteger amount;
    Timestamp periodStart;
    Timestamp periodEnd;
    Transaction transaction+;
}

value LoanRepayment
{
    Loan loan;
    PositiveInteger amount;
    AccountTransfer payment;
    Transaction transaction+;
}

value LoanDischarge
{
    Loan loan;
    PositiveInteger amount;
    Person authorisedBy;
    Transaction transaction+;
}

value LenderChange
{
    Loan loan;
    Person previousLender;
    Person newLender;
    PositiveInteger amount;
    Transaction transaction+;
}

value BorrowerChange
{
    Loan loan;
    Person previousBorrower;
    Person newBorrower;
    PositiveInteger amount;
    Transaction transaction+;
}

variant LoanChange
{
    LoanIncrease increase;
    InterestAccrual interest;
    LoanRepayment repayment;
    LoanDischarge discharge;
    LenderChange lenderChange;
    BorrowerChange borrowerChange;
}

Each loan change produces equal changes on the Claim and Liability sides. Creation, an additional advance and interest increase both balances by the same amount. Repayment and discharge reduce both by the same amount and cannot reduce either below zero. A lender change transfers the corresponding Claim quantity; a borrower change transfers the corresponding Liability quantity. A borrower change requires acceptance by the incoming borrower and any lender consent required by the contract.

The outstanding amount of a loan is derived from its history of increases, interest, repayments and discharges. The following invariant must always hold:

\[ \operatorname{claimBalance}(L) =\operatorname{liabilityBalance}(L) =\operatorname{outstanding}(L) \geq 0. \]

Purchases and escrow

The purchased property is described by an account unit and positive quantity. The escrow account is a Rune Property account owned by the purchaser. CATS restricts the use of its balance according to the referenced purchase contract, but neither CATS nor the seller owns the escrowed Runes before release.


value PurchaserReceipt
{
    Person purchaser;
}

value DispatchProof
{
    Person carrier;
}

value CustodyHandoverProof
{
    Person carrier;
}

value TimedRelease
{
    Timestamp releaseAt;
}

value AdjudicatedRelease
{
    String adjudicationRule;
}

variant EscrowReleaseCondition
{
    PurchaserReceipt purchaserReceipt;
    DispatchProof dispatchProof;
    CustodyHandoverProof custodyHandoverProof;
    TimedRelease timedRelease;
    AdjudicatedRelease adjudicatedRelease;
}

entity EscrowPurchase
{
    Integer id;
    Person purchaser;
    Person seller;
    Account escrowAccount;
    AccountUnit productUnit;
    PositiveInteger productQuantity;
    PositiveInteger price;
    Contract terms;
    EscrowReleaseCondition releaseCondition;
    Timestamp maximumDeliveryTime;
    key {id};

    constraints
    {
        escrowAccount.owner = purchaser;
        escrowAccount.role = property;
        escrowAccount.unit.rune.Σexists;
    }
}

The release condition is a variant because its alternatives require different evidence. The contract may require the purchaser's signed receipt, proof of dispatch, proof of a specified custody handover, expiry of an agreed time, or an adjudicated decision. More elaborate contracts can refer to a separate expression combining several conditions.

Escrow outcomes are also mutually exclusive. A released purchase records both sides of the exchange; a cancelled purchase records why the purchaser regains unrestricted use of the Runes.


value EscrowRelease
{
    EscrowPurchase purchase;
    AccountTransfer runeTransfer;
    AccountTransfer productTransfer;
    Transaction transaction+;
}

value EscrowCancellation
{
    EscrowPurchase purchase;
    String reason;
    Transaction transaction+;
}

variant EscrowOutcome
{
    EscrowRelease released;
    EscrowCancellation cancelled;
}

Before release, the purchaser owns the escrowed Runes and the seller owns the Product. A valid release transfers the Runes to the seller and ownership of the Product to the purchaser. Where the Product is not yet in the purchaser's custody, the release also creates a product loan whose lender is the purchaser and whose borrower is the Person responsible for delivery. If ownership and custody pass together on confirmed receipt, there is no outstanding product loan after release.

Custody of identified property

Ownership and custody are separate. For an identified item, custody is derived from a chain of accepted handovers. The predecessor reference prevents two different handovers from both validly following the same current handover.


entity CustodyHandover
{
    Integer id;
    IdentifiedItem item;
    Person previousCustodian;
    Person newCustodian;
    CustodyHandover predecessor?;
    Transaction transaction+;
    key {id};
}

The first handover has no predecessor. Every later handover must name the current final handover for the item, the previous custodian must equal its new custodian, and no committed handover may already use that predecessor. The incoming custodian authorises acceptance. If accepting custody also makes that Person responsible for delivery, the same commercial operation includes the corresponding borrower change for the product loan.

Operations and derived state

The different operation payloads can be brought together in a final variant. A commercial operation contains one or more such operations and refers to the local transactions which implement them. All entries within each local transaction either commit together or do not commit. Transactions on different Persons' nodes are linked by identifiers and signed proofs rather than forming one distributed atomic transaction.


variant CATSOperation
{
    AccountTransfer accountTransfer;
    LoanChange loanChange;
    EscrowOutcome escrowOutcome;
    CustodyHandover custodyHandover;
}

entity CommercialOperation
{
    Integer id;
    Transaction transaction+;
    CATSOperation operation+;
    key {id};
}

Balances, outstanding loan quantities, current ownership, current custody and escrow status are derived from these append-only records. They may be materialised and indexed for efficiency, but a materialised value is a cache rather than an independent fact. Corrections, refunds, returns, forgiveness and reversals are represented by new records referring to the records they affect.

The principal global invariants expressed by the Predica model are therefore:

Every account has exactly one immutable owner, role and unit.
Every derived account balance is a non-negative integer.
An account transfer preserves the role, unit and quantity transferred.
The Claim and Liability sides of every loan have the same unit and outstanding quantity.
An identified item has at most one current owner and at most one current custodian.
Escrowed Runes remain the purchaser's property until a valid release transfers them.
An escrow release transfers both the Runes and ownership of the purchased property.
No append-only event is deleted or altered after commitment.

PreviousChapter 16: Commerce Account and Transaction System (CATS) NextChapter 17: Tax