Statoblast and Zoltar invariants

An invariant is a statement that must remain true at every successful external-call boundary, across every legal lifecycle transition, or under the economic assumptions named beside it. Reverts may interrupt a transition, but they must roll back all of its state and asset effects.

The catalog separates local contract guards, automated release-tooling guards, cross-contract properties, and economic assumptions. Each entry names the strongest enforcement and evidence currently present; a documented implementation choice is not automatically a safe invariant.

See the Statoblast security model for assumptions A01–A28. Funded and underfunded clearing are explained in the Collateral Repair Auction clearing guide.

Invariant DependencyCorrect callers are necessary but insufficient. Their actions must conserve assets, every mandatory state transition must remain reachable, and the named participation and inclusion assumptions must hold where the protocol deliberately relies on economic incentives.

MatchesAll invariants listed below

Classification and scope

Each entry separates the kind of property from its current enforcement status. A status describes the strongest claim supported by the local implementation and tests; it is not a formal proof.

Type Meaning
Safety A forbidden caller, state, transition, or replay cannot succeed.
Conservation Assets, liabilities, supplies, and claims reconcile without duplication or loss.
Liveness A required permissionless action remains executable under the stated conditions.
Enforcement status Meaning
Contract guard A direct authorization, bound, or state check enforces the property locally.
Reviewed preservation Several contracts cooperate to preserve the property in reviewed flows and tests.
External assumption Solidity cannot guarantee the property without honest participation, liquidity, transaction inclusion, or external token behavior.
Automated tooling guard Release, deployment, or CI tooling rejects a mismatched artifact, address, or runtime-code identity before it is accepted.

The index lists the core universe properties and portfolio accounting boundaries. Identifiers name the property being reviewed; they are not contract entrypoints.

Terms used in the catalog

Pool question
The question whose outcome determines the SecurityPool's winning outcome shares and Escalation Game payouts.
Fork question
The ended question recorded by the universe fork. It may differ from the pool question.
Child branch
A well-formed answer encoding for the fork question, used to derive one child universe from its parent. SecurityPool's binary pool-question paths specifically use Invalid, Yes, and No.
Continuation game
A child Escalation Game initialized from an unresolved parent game's fork snapshot. Its child pool is in fork continuation until the game is fully resumed; the game itself remains the continuation game afterward.
Carry
The unresolved parent escalation deposits exported into a fork snapshot and paid out by continuation games against Merkle Mountain Range proofs.
Nullifier
A continuation game's record that one carried deposit identity has been consumed, so its proof cannot be replayed.
Fixed payout outcome
The pool-question outcome a continuation game must use after its deadline, regardless of its copied balance leader.
Direct fork
A caller invokes Zoltar's universe-fork entrypoint directly rather than through a pool's own non-decision path.
Recursive fork
A fork of a child universe created by an earlier fork.
Tracked balance
An amount recorded by protocol accounting; it excludes unsolicited assets unless a named transition explicitly credits them.
Consumed claim
A deposit, bid, or proof that has already been settled, refunded, exported, or otherwise made unusable.

Invariant index

Identifier Property Type Enforcement status
UNI-01 One fork per universe Safety Contract guard
UNI-02 Valid fork questions Safety Contract guard
UNI-03 Fork threshold burn and credit Conservation Contract guard
UNI-04 Deterministic child universe IDs Safety Contract guard
UNI-05 Well-formed child outcomes Safety Contract guard
UNI-06 Per-child migration mint limit Safety Contract guard
UNI-07 Branch-specific child REP Conservation Reviewed preservation
UNI-08 Child theoretical supply snapshot Conservation Reviewed preservation
UNI-09 Child REP supply coherence Conservation Reviewed preservation
QST-01 Question registry and classifier coherence Safety Reviewed preservation
AUTHORITY Portfolio identity and question admission Safety Contract guard and regression tests
POOL-ACCOUNTING Separate capital, settlement and reporter custody Safety Contract guard and regression tests
CAPITAL-HEALTH Owner commitments and loss isolation Safety Contract guard and regression tests
CAPITAL-EXIT Retirement and withdrawal accounting Safety Contract guard and regression tests
SHARE-SETTLEMENT Question shares and backing floor Safety Contract guard and regression tests
ESCALATION Reporter liabilities and historical proofs Safety Contract guard and regression tests
FORKS Shared fork choices and lazy questions Safety Contract guard and regression tests
AUCTIONS Uniform branch auction and automatic owners Safety Contract guard and regression tests
AUCTION-REFUNDS Bid and refund ownership Safety Contract guard and regression tests
ORACLE Shared price acceptance and exposure Safety Contract guard and regression tests
LIFECYCLE Bounded work and explicit recovery Safety Contract guard and regression tests
EXTERNAL-CALLS Authority before external effects Safety Contract guard and regression tests

Zoltar invariants

These properties govern core universe creation, REP supply, universe forks, deterministic child identities, and branch-specific REP migration.

Universes, REP supply, and migration

UNI-01One fork per universe

Required property

An initialized universe records at most one fork time and one fork question.

Example: After a universe forks on question 17, a second call attempting to fork it on question 22 reverts.

Type
Safety
Enforcement status
Contract guard
Primary evidence
Zoltar.forkUniverse
UNI-02Valid fork questions

Required property

forkUniverse accepts only a question that exists in ZoltarQuestionData and whose end time has been reached (block.timestamp >= endTime). A pool may separately require the fork question to equal its pool question. Zoltar intentionally imposes no question-creation age, universe registration, or pool-relevance condition.

Example: At exactly a known question's end time, a caller may fork a universe even when that question came from another universe or was created with an already-past end time; an unknown or still-open question is rejected. Requiring a universe-relevant or sufficiently aged question is not a Zoltar invariant.

Type
Safety
Enforcement status
Contract guard
Related assumption
A15 intended question selection
UNI-03Fork threshold burn and credit

Required property

The fork threshold is ⌈parent theoretical supply / forkThresholdDivisor⌉ for nonzero supply, and zero only when supply is zero. Starting a fork burns that amount of the initiator's parent REP, reduces the parent theoretical supply by the same amount, and credits the threshold minus ⌊threshold / forkBurnDivisor⌋ for migration. The configured forkBurnDivisor is at least 5, so the uncredited fork haircut cannot exceed 20%.

Example: With a 1,000 REP theoretical supply, threshold divisor 20, and burn divisor 5, the initiator commits 50 parent REP, pays a 10 REP fork haircut, and receives 40 REP of migration credit.

Type
Conservation
Enforcement status
Contract guard
UNI-04Deterministic child universe IDs

Required property

A child universe identity is exactly the truncated hash of its parent universe and fork outcome; one parent-outcome pair maps to one child.

Example: Repeatedly deriving the Yes child of the same parent returns the same universe ID, while deriving its No child returns a different ID.

Type
Safety
Enforcement status
Contract guard
UNI-05Well-formed child outcomes

Required property

Only well-formed outcomes of the recorded fork question can deploy child universes or receive migrated REP.

Example: For a binary categorical fork question whose valid indexes are 0, 1, and 2, passing index 3 cannot deploy a child or receive child REP.

Type
Safety
Enforcement status
Contract guard
UNI-06Per-child migration mint limit

Required property

For one migrator and one child, cumulative child REP minted never exceeds that migrator's parent migration balance.

Example: A migrator with 40 REP of migration credit cannot mint 25 REP and later mint another 20 REP into the same child.

Type
Safety
Enforcement status
Contract guard
UNI-07Branch-specific child REP

Required property

One burned parent migration balance may mint the same credited amount into several selected children. Each minted balance belongs to a different child REP token, and migration never restores the burned parent REP.

Example: A 40 REP migration credit may mint 40 Yes-child REP and 40 No-child REP, but neither balance is parent REP and the burned parent balance remains zero.

Type
Conservation
Enforcement status
Reviewed preservation
Primary evidence
_splitRep, ReputationToken
UNI-08Child theoretical supply snapshot

Required property

The child theoretical-supply snapshot equals the parent's theoretical supply after the threshold burn plus the initiator's migration credit net of the fork haircut. Each child therefore excludes the uncredited fork haircut.

Example: If a fork removes 50 parent REP and credits 40 migration REP, each child's theoretical snapshot is 10 REP below the pre-fork supply.

Type
Conservation
Enforcement status
Reviewed preservation
UNI-09Child REP supply coherence

Required property

For each child REP token, total minted supply equals the sum of holder balances, never exceeds the child's theoretical-supply snapshot, and uses the same theoretical maximum recorded by the child universe.

Example: If two migrators mint 12 and 7 child REP, the child token supply is 19 REP, both balances sum to 19 REP, and minting does not change the child's theoretical maximum.

Type
Conservation
Enforcement status
Reviewed preservation

Questions and answer classification

QST-01Question registry and classifier coherence

Required property

Every successful question creation appends its deterministic ID exactly once and leaves prior question data and labels immutable. For every stored question and answer, the malformed classifier is true exactly when the public answer name is Malformed, except that a categorical question may use the literal label Malformed for a well-formed outcome.

Example: Appending a scalar question after two categorical questions preserves the first two records and their order; a scalar answer with reserved bits is both classified and named malformed.

Type
Safety
Enforcement status
Reviewed preservation

Shared portfolio invariants

These properties apply to every portfolio, including fixed one-question portfolios. The module reference describes the corresponding accounting and authority boundaries.

AUTHORITYPortfolio identity and question admission

Required property

The canonical factory namespace binds every question ledger to its portfolio. The immutable admission policy controls registration. A fixed one-question portfolio uses the same capital, settlement and reporting contracts as an open portfolio.
Type
Safety
Enforcement status
Contract guard and regression tests
Primary evidence
SecurityPoolPortfolio.sol
POOL-ACCOUNTINGSeparate capital, settlement and reporter custody

Required property

Provider REP and commitments belong to the capital ledger; question cash and outcome supply belong to the settlement book; reporter REP belongs to the reporter ledger. A reporting deposit does not acquire underwriting rights, and a trader purchase does not create a provider position.
Type
Safety
Enforcement status
Contract guard and regression tests
CAPITAL-HEALTHOwner commitments and loss isolation

Required property

Each owner authorizes its commitment and health target. Health counts that owner’s free and pledged principal against its full commitment. A liquidation affects the target’s position; other owners do not absorb its penalty. Unvested REP income is excluded from principal health.
Type
Safety
Enforcement status
Contract guard and regression tests
CAPITAL-EXITRetirement and withdrawal accounting

Required property

An owner cannot withdraw principal needed by its live commitment or pending risk. Retirement immediately removes capacity available to new purchases while the settlement book tracks when the old demand becomes releasable. Owners do not claim separately for every question.
Type
Safety
Enforcement status
Contract guard and regression tests
SHARE-SETTLEMENTQuestion shares and backing floor

Required property

Each question has its own outcome shares and cash entitlement. Purchases check healthy aggregate capacity and the configured minimum backing floor. Complete-set returns release their demand; fees stop before settlement backing would fall below the floor. Finalized claims use their protected settlement state.
Type
Safety
Enforcement status
Contract guard and regression tests
ESCALATIONReporter liabilities and historical proofs

Required property

Ordinary settlement fixes winning payout liabilities and required burns before paying individual claims. Inherited claims authenticate frozen Merkle-mountain-range membership and per-branch nullifiers. Consumed principal compacts exported principal intervals; reward coordinates remain unchanged. Replaying a consumed proof cannot pay again.
Type
Safety
Enforcement status
Contract guard and regression tests
Primary evidence
EscalationGameSettlement.sol
FORKSShared fork choices and lazy questions

Required property

Each owner records one branch choice before the fixed cutoff. Shared books snapshot the branch once; question ledgers and reporter snapshots are materialized on demand. Materialization cannot extend the native choice, auction or activation deadlines.
Type
Safety
Enforcement status
Contract guard and regression tests
AUCTIONSUniform branch auction and automatic owners

Required property

Only freshly unchosen provider REP is auction inventory; reporter escrow and previously owed recovery REP are excluded. Winners pay the same grid-rounded REP-per-lot price. Winning principal and obligations enter aggregate accounting at closing even if a bidder delays activating individual controls.
Type
Safety
Enforcement status
Contract guard and regression tests
AUCTION-REFUNDSBid and refund ownership

Required property

Early refund eligibility must be proven by the auction’s irreversible losing condition. Refund credits belong to the bidder and are withdrawn independently of winner activation. The auction cannot require an unbounded scan of losing bids before honest winners can act.
Type
Safety
Enforcement status
Contract guard and regression tests
ORACLEShared price acceptance and exposure

Required property

Independent report candidates cannot reserve exclusive access. Acceptance checks price freshness, funded coverage and the portfolio reporting window and atomically checkpoints capital under the previous price. A rejected or disputed renewal cannot extend the accepted price’s expiry.
Type
Safety
Enforcement status
Contract guard and regression tests
Primary evidence
SharedPoolPriceFeed.sol
LIFECYCLEBounded work and explicit recovery

Required property

Capital and settlement operations use fixed-width indexes and aggregate accounting rather than scanning every owner or question. User-supplied claim batches are divisible. Deep inherited claims may require bounded checkpoint transactions, but do not force unrelated owners to process their history.
Type
Safety
Enforcement status
Contract guard and regression tests
EXTERNAL-CALLSAuthority before external effects

Required property

Canonical module bindings and caller guards protect delegated accounting. Transaction failures roll back coupled state changes. External REP and oracle assumptions remain explicit in the security model; these invariants do not guarantee an honest market price or transaction inclusion.
Type
Safety
Enforcement status
Contract guard and regression tests
Primary evidence
SecurityPoolPortfolio.sol