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.
Supply and balances
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
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
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
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
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
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
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
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.
Last updated