> For the complete documentation index, see [llms.txt](https://docs.t-rex.network/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://docs.t-rex.network/security-and-trust-model/invariants.md). # Invariants An invariant is a property that holds at all times, whatever sequence of calls is made and whoever makes them. This page lists the invariants of the protocol. They are what an auditor checks, what an indexer can rely on, and what an integrator can assume without reading the code. Each invariant is stated once, with where it is enforced. How the invariants are tested is described in [Audits and verification](/security-and-trust-model/audits-and-verification.md). ## Supply and balances | # | Invariant | Enforced by | | -- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | -------------------------------------------------------------------------------------------- | | S1 | **The supply moves only by a mint or a burn.** `totalSupply` equals everything minted less everything burned. No transfer, freeze, delegation, recall or settlement changes it. | `Token` | | S2 | **The balances on the reference chain add up to the native supply.** The sum of every `balanceOf` equals `totalSupply() - totalBridged()`. | `Token` | | S3 | **Frozen never exceeds the balance.** For every address, `getFrozenTokens` is at most `balanceOf`. The free balance is never negative. | `Token`: freezing more than the balance reverts, and so does unfreezing more than is frozen. | | S4 | **The supply is conserved across the parts.** `totalSupply` equals the sum of free, frozen and bridged amounts, in-transit amounts included. | `Token` | | S5 | **The bridged supply is what the satellite wallets hold, plus what is in transit.** `totalBridged` equals the sum of every `bridgedBalanceOf` plus `totalInTransit`. | `Token` | | S6 | **The token holds no escrow.** The token contract's own balance is zero. Bridged positions are recorded, not held. | `Token` | ## The gates | # | Invariant | Enforced by | | -- | -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ------------------------------------ | | G1 | **No tokens reach an unverified recipient.** Every transfer, mint and forced transfer requires `isVerified(to)`. | `Token`, calling `TREXRegistry` | | G2 | **No movement by a holder exceeds what the rules allow.** Every transfer and every mint requires `canTransfer`. | `Token`, calling `ModularCompliance` | | G3 | **No transfer between holders executes while the token is paused.** This includes forced transfers, recoveries and settlements. | `Token` | | G4 | **A frozen address neither sends nor receives a transfer, and a transfer never spends frozen tokens.** | `Token` | | G5 | **A refused spender spends nothing.** When a spender module refuses a caller, `transferFrom` reverts before the allowance is touched. | `Token`, calling `ModularCompliance` | | G6 | **The compliance of a token stays its compliance.** Once the token has supply, neither its compliance nor its registry can be replaced, and the compliance cannot be bound to another token. | `Token`, `ModularCompliance` | ## The compliance ledger | # | Invariant | Enforced by | | -- | ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ---------------------------- | | L1 | **A position is what the identity's addresses hold.** `positionOf(identity)` equals the balances on the reference chain plus the bridged positions, over every address of the identity. | `ModularCompliance` | | L2 | **Positions add up to the supply.** The sum of all positions plus `positionGap` equals `totalSupply`. | `ModularCompliance` | | L3 | **The gap is zero unless an agent changes a registration under a holding address.** Movements of tokens and an investor revoking a wallet leave it at zero. | `ModularCompliance` | | L4 | **Pending amounts are the open validations.** `pendingInOf` and `pendingOutOf` of an identity equal the sum of the maximum amounts of the validations that still reserve against it. Movements between two addresses of one identity reserve nothing. | `ModularCompliance` | | L5 | **A wallet's reservation is its open validations.** `reservedOf(wallet)` equals the sum of the maximum amounts of the open validations out of that wallet, and never exceeds its bridged position. | `Token`, `ModularCompliance` | | L6 | **A movement between two addresses of one identity changes no position.** | `ModularCompliance` | ## Validations | # | Invariant | Enforced by | | -- | -------------------------------------------------------------------------------------------------------------------------------------- | ------------------- | | V1 | **A satellite transfer is recorded only against a validation that was issued.** A settlement for an unknown validation is not applied. | `ModularCompliance` | | V2 | **A validation is settled once per chain.** A second settlement of the same half is not applied. | `ModularCompliance` | | V3 | **The settled amount is inside the issued range.** | `ModularCompliance` | | V4 | **The two halves of a transfer between satellites carry the same amount.** | `ModularCompliance` | | V5 | **A reservation is released exactly once**, at settlement, discard or resolution. | `ModularCompliance` | | V6 | **A validation is never issued for more than the sending wallet can send**, nor for more than the rules allow at that moment. | `ModularCompliance` | | V7 | **A validation with one half executed is never discarded.** | `ModularCompliance` | | V8 | **A settlement never expires.** A validation can expire. An execution that happened is always recorded when it is reported. | `ModularCompliance` | ## Messaging | # | Invariant | Enforced by | | -- | ------------------------------------------------------------------------------------------------------------------------------------------ | ----------------------------------------- | | M1 | **The token acts only on messages from its peer.** The author of an accepted message is the asset's T-REX Lite on the chain it comes from. | `Token` | | M2 | **The token acts only on messages delivered by a gateway the network trusts at that instant.** | `Token`, reading `TrustedGatewayRegistry` | | M3 | **A settlement is accepted only from the gateway its validation went out through.** | `Token` | | M4 | **A message is processed once per gateway.** | `Token` | | M5 | **A token sends nothing to a chain it was not opened for.** | `Token` | | M6 | **No role on a token can change the gateway registry it trusts.** | `Token` | ## Identity | # | Invariant | Enforced by | | --- | ---------------------------------------------------------------------------------------------------------------------------------------------------- | ------------------------------------------------------ | | I1 | **A wallet belongs to at most one identity, forever.** A wallet that was linked is never linked to another identity. | `IdentityFactory` | | I2 | **A revocation is terminal.** A revoked wallet is never linked again, and it keeps resolving to its identity for attribution. | `IdentityFactory` | | I3 | **A wallet has one entry.** Only the canonical encoding of an interoperable address is accepted. | `IdentityFactory`, `Token` | | I4 | **The type of an identity never changes**, and it is read from the factory, not from the identity. | `IdentityFactory` | | I5 | **An identity always has a manager that can sign.** The last such `MANAGEMENT` key cannot be removed, and an identity cannot be created without one. | `ERC734Validator`, `IdentityFactory` | | I6 | **An `ACTION` key cannot perform a management operation**, through any path: user operation, direct call or execution queue. | `ERC734Validator`, `SmartAccount`, `KeyApprovalModule` | | I7 | **An identity holds at most one claim per issuer and topic.** | `ERC734Validator` | | I8 | **A claim that was revoked or removed cannot be added again with the same signature.** | `ERC734Validator` | | I9 | **An issuer writes only claims attributed to itself.** | `ERC734Validator` | | I10 | **A signature made for one identity is not valid for another.** Each identity has its own signing domain. | `Identity` | ## Access | # | Invariant | Enforced by | | -- | ----------------------------------------------------------------------------------------- | ------------------------------------- | | A1 | **Every privileged function reverts for a caller the access manager does not authorize.** | Every managed contract | | A2 | **A role of one domain authorizes nothing in another domain.** | Role identifiers, `TREXAccessManager` | | A3 | **Only the bound token notifies its compliance of a movement.** | `ModularCompliance` | | A4 | **Only the bound compliance settles a validation on the token.** | `Token` | | A5 | **Only a bound registry writes to an identity storage.** | `IdentityRegistryStorage` | | A6 | **A compliance binds at most 25 modules.** | `ModularCompliance` | | A7 | **A module accepts settings only from a compliance it is bound to.** | Compliance modules | ## Upgrades | # | Invariant | Enforced by | | -- | ------------------------------------------------------------------------------ | ----------------------------- | | U1 | **A shared suite never moves to an older version.** | `TREXImplementationAuthority` | | U2 | **A published version never changes.** | `TREXImplementationAuthority` | | U3 | **The five contracts of a shared suite are always of the same version.** | `TREXImplementationAuthority` | | U4 | **An upgrade of identities keeps the same factory and the same key registry.** | `IdentityFactory` | ## What is not an invariant Three things that are sometimes assumed and do not hold. * **A holder is always eligible.** Eligibility is checked when a position is received. A holder can lose it afterward, when a claim expires or is revoked, and keep its position. * **The balance on a satellite equals the bridged position at every instant.** They differ between an execution on the satellite and its settlement. * **Positions always respect every rule.** Agent operations bypass the rules by design. A forced transfer, or a settlement applied late, can leave a position that a rule would not have allowed. The compliance is told, so that the ledger stays correct and the next movement is judged against the real state. The Issuer then resolves the breach. --- # Agent Instructions This documentation is published with GitBook. GitBook is the documentation platform designed so that both humans and AI agents can read, navigate, and reason over technical content effectively. Learn more at gitbook.com. ## Querying This Documentation If you need additional information that is not directly available in this page, you can query the documentation by asking a question. Perform an HTTP GET request on the following URL with the `ask` and `goal` query parameters: ``` GET https://docs.t-rex.network/security-and-trust-model/invariants.md?ask=&goal= ``` `ask` is the immediate question: it should be specific, self-contained, and written in natural language. `goal` is what the user is ultimately trying to achieve, the reason they need the answer. Sharing it helps GitBook give you a better, more relevant answer. A goal is most helpful when it describes the outcome the user wants rather than restating the question. For example, with `ask=how do I create an API token`, a goal like `automate deployments from our CI pipeline` lets GitBook tailor the answer to that use case. The response will contain a direct answer to the question and relevant excerpts and sources from the documentation. Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.