9. Invariants

Repository

bloque-app/aledgent

Commit

5ca6b8a

Version

0.4.27

Status

draft

Rendered

2026-10-17T19:30:18Z

Source

SPEC.md, last changed in 5ca6b8a

Each invariant names the layer that MUST enforce it. REQ-AR-4 forbids satisfying one at a weaker layer. The Enforced by column is the target. The V0 column is where the first release enforces the invariant (REQ-AR-6). Where V0 names a weaker layer than the target, an amendment records it, as REQ-AR-4 requires (amendment 0006 names INV-15, INV-16 and INV-22). The layers are:

• Store: the enforcement survives any application change.
• Kernel: the accounting core makes a violation impossible to express.
• Service: aledgent’s own logic.
• Credential: a cryptographic property, not a check.

ID	Invariant	Enforced by	V0
INV-1	For every posting and every asset, debits equal credits. A single-legged posting cannot be expressed.	Kernel	Kernel
INV-2	The book is append-only. No committed entry or posting is ever changed or deleted. A correction is a new posting.	Kernel + store	Kernel + store
INV-3	A Customer account is never negative, in any asset or balance kind, at any instant, under any concurrency.	Kernel	Kernel
INV-4	Assets are kept separate within an account. No operation mixes the balances of two assets.	Kernel	Kernel
INV-5	Across the whole book, the signed sum of all entries for each asset is exactly zero.	Store (continuously checked)	Store (continuously checked)
INV-6	Every stored balance equals the sum of the entries that produced it. It can be re-derived from entries alone.	Store + service	Store + service
INV-7	Every monetary amount is an exact integer count of a registered asset’s minor units, at every boundary.	Store + type	Store + type
INV-8	There is exactly one authoritative copy of every ledger fact, and it belongs to aledgent.	Service	Service
INV-9	An account that exists can be credited. No state exists in which an account exists and an inbound credit to it is discarded.	Service	Service
INV-10	No entry is written against the issuance counterparty for an external leg before that leg is final.	Service	Service
INV-11	No caller can assert an operation’s outcome. aledgent derives every outcome from evidence it recorded.	Service	Service
INV-12	An observation coordinate is applied at most once, permanently.	Store	Store
INV-13	No external leg can execute on a path that has not reserved first.	Service	Service
INV-14	A reservation and its capture or release are the same object, matched by identity. An amount supplied by a confirming party never decides what is released.	Service	Service
INV-15	No non-terminal operation exists without a deadline and a resolution path the operator can reach. Past its deadline, that path is Needs-Review.	Store + service	Service
INV-16	A principal cannot reach any ledger fact it holds no authority over.	Store	Service
INV-17	No identifier and no anchored value contains personal data.	Store + build gate	Store + build gate
INV-18	Every state transition is idempotent on (operation, from-state, to-state, evidence).	Store	Store
INV-19	An anchor commits, at one consistent cut (REQ-RT-14), to every entry up to and including the cut’s commit of each partition (REQ-RT-9), to the registry of identities, credentials and grants at the cut’s version, to the audit trail up to the cut’s sequence of each writer (REQ-RT-13), and to each writer’s stream heads at the cut, and to nothing else.	Service	Service
INV-20	Every entry against an account is visible to that account’s authority holders. The authority that caused it is recorded.	Service	Service
INV-21	Terminal operation states are absorbing. An operation never leaves a terminal state.	Store	Store
INV-22	A credential cannot widen its own scope or change its own kind.	Credential	Service
INV-23	A refusal by the accounting core is never, on its own, a terminal outcome for an operation whose external leg can be observed independently.	Service	Service
INV-24	There is exactly one asset registry. An asset’s precision is recorded only there.	Store	Store
INV-25	A deployment has exactly one book. It is not split by asset, by account kind or by integrating party. Holding its state in partitions of accounts (REQ-RT-9) does not split it: one registry, one trial balance, one sequence of anchors.	Architecture	Architecture

INV-10, INV-11, INV-12, INV-13, INV-14 and INV-23 exist together so that the settlement layer and the book can never disagree about whether value moved:

• an outer success cannot be read as an inner one (INV-11);
• a release cannot be keyed on an amount instead of an identity (INV-14);
• an external leg cannot bypass the book (INV-13);
• an accounting refusal cannot be recorded as an external failure (INV-23).

---