Zoltar Protocol 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 from cross-contract properties and economic assumptions. It also records launch-critical properties that the current contracts do not preserve. A documented implementation choice is not automatically a safe invariant.

New to Zoltar's actors and fork lifecycle? Read Start Here before using this catalog as a contract or test reference.

The Protocol Security Model is normative for the accepted oracle assumption and truth-auction policy, the guarantees they exclude, and the residual loss allocation when the oracle assumption fails or auction demand is weak.

Protocol invariant layers Four connected layers run from local authority guards through cross-contract conservation and lifecycle liveness to economic security. A failure in an earlier layer invalidates the safety claims built above it. Authority canonical callers one-time wiring Conservation ETH, REP, shares claims and reserves Lifecycle legal transitions permissionless liveness Economics arbitrage incentives inclusion assumptions Each layer depends on every invariant to its left.

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.

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. Changes to any contract named in the evidence column must preserve the full statement, not only the check performed in one function.

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.
External assumption The property depends on participant behavior, inclusion, liquidity, or token behavior outside the contracts.
Enforcement status Meaning Required response
Contract guard A direct authorization, bound, or state check enforces the property locally. Keep the guard and test its negative boundary.
Reviewed preservation Several contracts cooperate to preserve the property in reviewed flows and tests. Protect it with cross-contract invariant and lifecycle tests.
Open violation A concrete sequence reaches a state that contradicts the required property. Fix before deployment and retain a regression test.
Economic or external assumption Solidity cannot guarantee the property without honest participation, liquidity, or transaction inclusion. State and monitor the assumption, and document both its failure mode and the guarantees deliberately excluded from the protocol model.
Proposed guard The property closes a missing safety or verification boundary not currently represented as one assertion. Add a contract check, model assertion, or invariant harness where practical.

Invariant identifiers are stable review labels. They are grouped by authority, universe, asset, share, vault, fork, escalation, oracle, auction, and lifecycle boundaries rather than by Solidity file.

Terms used in the catalog

Pool question
The question whose outcome determines the pool's winning shares and escalation 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.
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.

Remediated Launch Findings

These properties had confirmed failure paths in the audited implementation. The current implementation enforces them and retains focused regression coverage. Their stable identifiers remain in this catalog so future changes preserve the fixes. The summaries below record prior defects and repairs; each linked catalog entry is the authoritative invariant statement and contains its single example.

ID Preserved rule summary Current enforcement
FORK-04 Unsolicited REP at a migration-proxy address cannot block or change pool fork initiation. The forker migrates only the REP received from the pool or escalation game during the call and checks the migration-ledger delta. Prefunded proxy REP remains isolated in both external- and own-fork paths.
SHARE-04 Complete-set collateral accounting and winning-share redemption each use the supply denominator for the claims they settle. Child setup copies the frozen parent's remaining economic claim supply. That denominator reserves collateral for materialized ERC-1155 balances and source entitlements that can materialize later; complete-set and winning-share redemption consume it.
BAL-02 Unsolicited ETH cannot alter collateral accounting or block a required transition. Collateral is tracked independently from raw balance. Fork migration and auction finalization add only protocol-routed ETH, leaving forced ETH as unaccounted surplus.
SHARE-03 Every successful positive-value complete-set mint creates a positive quantity of every outcome share. A zero-supply pool can bootstrap only with zero tracked collateral, and a mint that would calculate zero shares reverts without changing accounting.
AUC-07 Weak-demand winners receive the complete REP sale cap at one effective price, while every other bid refunds. Qualifying underfunded demand shares maxRepBeingSold in proportion to retained ETH. With no qualifying demand, every bid refunds after value-free finalization.
ESC-12 A child pool and its continuation game agree on the outcome used to settle carried deposits through direct and recursive forks. A branch selected by a matching fork becomes the immutable continuation outcome, later universe forks cannot transition that fixed pool, and escalation-deposit withdrawal rejects a pool/game mismatch.
ESC-13 Two outcomes cannot both reach non-decision with less REP than the universe fork threshold. The non-decision threshold is ceil(forkThreshold / 2), including odd fork thresholds.
AUC-10 Deleting and later recreating an auction tick cannot corrupt a later bid's cumulative position or make its ETH unclaimable. Bid history remains append-only, cumulative ETH continues across tick recreation, and the refund-prefix tree subtracts every previously refunded bid.

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.

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.

UNI-03Fork threshold burn and credit

Required property

The fork threshold is floor(parent theoretical supply / forkThresholdDivisor). 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 floor(threshold / forkBurnDivisor) for migration.

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 haircut, and receives 40 REP of migration credit.

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.

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.

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.

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.

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 post-haircut migration credit. 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.

Augur Statoblast Invariants

These properties govern Statoblast deployment, SecurityPool accounting, fork migration, escalation, oracle operations, truth auctions, and the cross-contract lifecycle built on Zoltar universes.

Authority and Deployment Identity

AUTH-01Coordinator and forker-only operations

Required property

Only the immutable coordinator may execute price-sensitive pool operations, and only the immutable forker may mutate fork accounting or transfer migration assets.

Example: A wallet calling performWithdrawRep directly is rejected because only the coordinator may call it.

AUTH-02Atomic pool and coordinator binding

Required property

The pool and its coordinator bind once during atomic factory deployment; no external caller gets a transaction boundary in which it can install a substitute pool.

Example: A caller cannot front-run factory deployment and make the coordinator point to an attacker-controlled pool.

AUTH-03Immutable protocol logic

Required property

No mutable owner, governance address, upgrade implementation, or emergency operator can replace protocol logic after deployment.

Example: After deployment, no administrator can point a pool proxy at different bytecode because the pool has no upgrade slot.

AUTH-04Deterministic deployment identity

Required property

Every canonical CREATE2 address commits to the correct factory, salt, constructor arguments, parent identity, universe, question, and multiplier.

Example: Changing a child's question ID changes its derived address instead of deploying different semantics at the expected address.

AUTH-05Delegate storage compatibility

Required property

Delegatecall targets are constructor-installed protocol modules, and every target interprets the forker's storage with the same layout.

Example: The vault-migration delegate reads forkDataByPool from the same slot used by the forker rather than corrupting adjacent state.

AUTH-06Permissionless settlement beneficiaries

Required property

Anyone may trigger permissionless settlement, but the caller cannot choose its beneficiary. Each transfer or ownership credit goes only to the vault, bidder, depositor, or share holder recorded for that claim.

Example: Alice may settle Bob's auction bid, but the purchased REP and ownership are credited to Bob's vault.

AUTH-07Published deployment verification

Required property

For every published deployment address, the runtime-bytecode hash and constructor-installed dependencies must match the reviewed release manifest.

Example: A manifest check fails when the published coordinator address contains code built with a different OpenOracle dependency.

Pool Assets, Shares, and Vaults

The raw ETH balance needs an explicit surplus term. Without it, forced ETH is indistinguishable from collateral and can change an exchange rate or lifecycle precondition.

rawEthBalance = completeSetCollateral + unallocatedFeeReserve + totalFeesOwedToVaults + explicitSurplus

ETH Conservation BoundaryEvery successful external call should reconcile raw ETH into named liabilities or an explicit surplus bucket. Raw balance alone must not define collateral.

BAL-01ETH conservation

Required property

At every successful external-call boundary, raw ETH = tracked collateral + unallocated fee reserve + total vault fee debt + unaccounted surplus. Surplus is the derived remainder and is never a protocol liability.

Example: If the pool holds 12 ETH, owes 2 ETH in fees, and tracks 9 ETH of collateral, the remaining 1 ETH is surplus rather than additional collateral.

BAL-02Unsolicited ETH isolation

Required property

Unsolicited ETH cannot change collateral, initialize an exchange rate, increase liabilities, or block a required transition.

Example: ETH forced into an empty pool does not let the first complete-set mint use that ETH as its collateral base.

BAL-03Collateral capacity

Required property

Tracked complete-set collateral never exceeds total security-bond allowance. Fee checkpointing and redemption cannot reclassify unsolicited ETH as collateral.

Example: With 10 ETH of bond allowance, a mint that would raise tracked collateral from 9 ETH to 11 ETH reverts even if the raw balance contains surplus ETH.

BAL-04REP coverage boundaries

Required property

At the latest valid REP-per-ETH price, increasing an allowance requires REP coverage strictly above the requested obligation; withdrawing REP may leave coverage exactly equal to the existing obligation. The security multiplier is applied only by the named liquidation and transfer checks, not a second time in these coverage comparisons.

Example: At 100 REP per ETH, withdrawing to 100 REP against an existing 1 ETH allowance is permitted, but setting a new 1 ETH allowance with only 100 REP fails the strict check.

BAL-05REP ownership conversion consistency

Required property

After deposits, withdrawals, liquidations, escalation transfers, migration, and auction claims, the same current pool REP balance and ownership denominator govern both REP-to-ownership and ownership-to-REP conversion.

Example: Depositing REP and immediately converting the resulting ownership back to REP uses the same denominator rather than a stale pre-deposit balance.

BAL-06Fee liability accounting

Required property

Every accrued fee wei is represented once as unallocated reserve or vault debt, and redemption clears the debt before ETH is sent.

Example: Assigning 3 wei of reserve to a vault decreases unallocated reserve by 3 and increases that vault's debt by 3, without creating a second claim.

BAL-07Fee reserve protection

Required property

Fork transfers and redemptions cannot spend ETH reserved for unpaid or unallocated fees.

Example: A fork transfer may move 8 ETH of collateral from a 10 ETH balance that also contains 2 ETH of fee liabilities, but may not move all 10 ETH.

SHARE-01Complete-set symmetry

Required property

A complete-set mint or burn changes Invalid, Yes, and No balances by the same amount in the same universe.

Example: Minting five complete sets creates five Invalid, five Yes, and five No shares for that universe.

SHARE-02Complete-set redemption

Required property

Before outcome finalization, burning B complete sets returns floor(B × tracked collateral / complete-set supply) after the fee checkpoint, then reduces supply by B and collateral by the ETH returned.

Example: With 100 sets and 10 ETH of tracked collateral, burning 10 sets returns 1 ETH before integer-rounding residue.

SHARE-03Positive-output minting

Required property

A successful positive-value complete-set mint returns a positive share amount.

Example: A 1 wei mint that rounds to zero shares reverts instead of accepting the ETH.

SHARE-04Child supply denominators

Required property

Child setup copies the frozen parent's remaining economic claim supply as its collateral denominator. That supply includes both materialized child ERC-1155 balances and source entitlements that can materialize later. Complete-set minting adds claims, while complete-set and winning-share redemption consume them.

Example: If a parent freezes with 10 claims per outcome and a child has no materialized shares yet, setup still records 10. A new minter receives only the shares purchased at that established rate, while all 10 source claims retain their reserved collateral.

SHARE-05Winning-share payout cap

Required property

Total ETH paid to winning shares never exceeds the collateral available when redemption begins; rounding residue remains for later winning holders.

Example: When two winners redeem sequentially, the second receives its fraction of the collateral left after the first rather than a fraction of the original balance paid twice.

VAULT-01Escrowed REP isolation

Required property

REP escrowed in an escalation game cannot also be withdrawn, liquidated as unlocked REP, or migrated as unlocked vault ownership.

Example: A vault with 20 REP deposited and 5 REP escrowed cannot make an ordinary withdrawal while that escrow remains; unlocked-state migration can move only the other 15 REP, while the escrow claim follows its separate migration path.

VAULT-02Liquidation conservation and freshness

Required property

A liquidation transfers rather than creates aggregate ownership and allowance. The resulting liquidator and target vaults must meet coverage and minimum-size rules, and execution must reject a target whose protected ownership or allowance changed after staging.

Example: If the target reduces its ownership after a liquidation is staged, execution rejects the stale snapshot instead of transferring the originally quoted amount.

Forks and Child Isolation

FORK-01Parent pool finality

Required property

Once the parent universe forks, parent operational flows freeze and the parent pool never re-enters Operational.

Example: After fork activation, the parent cannot accept another REP deposit or later return from PoolForked to Operational.

FORK-02Immutable fork snapshot

Required property

When the parent first enters fork mode, it captures fork time, collateral, REP buckets, ownership denominator, escalation state, and allowance exactly once. Those immutable values are the common basis for every child of that fork.

Example: REP sent unsolicited to the parent after fork mode begins cannot change the REP snapshot used to initialize a later-created No child.

FORK-03Isolated migration proxy

Required property

Each parent pool maps to exactly one deterministic migration-proxy address, and that address is the pool's isolated identity in the Zoltar migration ledger.

Example: Two parent pools using the same forker derive different proxy addresses and therefore cannot spend each other's migration credit.

FORK-04Prefunded proxy isolation

Required property

Preexisting or unsolicited REP at the deterministic proxy cannot block initiation or become unclassified migration principal.

Example: An attacker sending 1 REP to the future proxy address cannot make fork initiation revert or count that REP as pool migration principal.

FORK-05Eight-week migration boundary

Required property

Child creation, vault migration, REP splitting, and own-fork claims are allowed through forkActivationTime + 8 weeks, inclusive, and are closed after that timestamp. forkActivationTime is recorded when the parent pool enters PoolForked; post-migration activation begins only after its window ends. Share materialization has no expiry, but after the deadline it can target only an already-created child.

Example: Vault migration succeeds exactly at the eight-week deadline and reverts one second later.

FORK-06Child deployment identity

Required property

A deployed child must name the requesting pool as its parent and must use the child universe derived from that parent's selected branch. Its factory, forker, auction, share token, pool question, and security multiplier must equal the values supplied or inherited by the parent factory path.

Example: The canonical factory installs the parent's share token, pool question, and multiplier in the child; the post-deployment guard then checks its parent, universe, factory, forker, and auction before linking it.

FORK-07Single-use unlocked vault migration

Required property

Migrating unlocked vault state credits one child and clears the corresponding parent ownership and allowance before it can be reused.

Example: After Alice migrates her unlocked position to the Yes child, a second migration call cannot credit the same parent ownership to the No child.

FORK-08One-time aggregate continuation backing

Required property

Each selected child initializes the canonical carry snapshot and receives the complete aggregate continuation backing at most once. Optional vault cleanup only clears parent locks; it creates no child escrow and cannot change carried-proof eligibility.

Example: Creating the Yes child installs its snapshot and aggregate backing before Alice acts. Alice may later clear her parent lock, but that cleanup neither funds the child nor enables or disables her winning proof.

FORK-09Cumulative child collateral

Required property

Cumulative parent ETH transferred to children never exceeds the fork collateral snapshot and is derived from cumulative migrated REP, not per-call rounding.

Example: If several calls collectively migrate R child REP, their collateral target is ceil(fork collateral × R / denominator), independent of how that same R is partitioned. The denominator is vaultRepAtFork for an own fork and auctionableRepAtFork otherwise.

FORK-10Share migration integrity

Required property

Share migration preserves the holder's parent token-ID balance as a persistent entitlement, rejects duplicate or malformed target outcomes, and mints only the unmaterialized balance into each selected child. A used source balance cannot transfer.

Example: Materializing seven parent Yes shares in one child leaves all seven parent entitlements visible and locked. A later call can mint seven into another existing child, but cannot mint the first child twice.

FORK-11Unequal child share supplies

Required property

Child pricing uses the fork-time economic claim supply rather than currently materialized outcome supplies. Unequal ERC-1155 supplies therefore do not block complete-set minting or proportional complete-set redemption. The denominator lifecycle and payout mechanics are owned by SHARE-04.

Example: If the economic supply is 12 while materialized supplies are 10, 8, and 6, a new complete set is priced against 12 and adds the same newly purchased balance to all three materialized supplies.

FORK-12Child activation after settlement

Required property

Value-free truth-auction settlement activates a child with its tracked migrated collateral plus retained auction ETH, which cannot exceed the parent fork snapshot. Fork-time economic claim accounting keeps later minting and proportional burns independent from materialization order.

Example: A child with 9 ETH against a 10 ETH fork snapshot activates after value-free finalization with 9 ETH of tracked collateral; its later operations remain subject to the ordinary share-supply and minting guards.

Escalation Games and Carried Claims

ESC-01Total escrow reconciliation

Required property

totalEscrowedRep equals the sum of live vault-denominated escrow records. Aggregate continuation backing is held by the child game but is not assigned to any vault escrow.

Example: If two vaults have live escrow records of 4 and 6 REP, totalEscrowedRep is 10 REP even when the game also holds aggregate REP backing for carried proofs.

ESC-02Local unresolved REP reconciliation

Required property

totalLocalUnresolvedRep equals the sum of unresolved local deposits, and each vault-local counter is its exact component.

Example: If Alice has 3 unresolved REP and Bob has 5, their counters are 3 and 5 and the global local-unresolved total is 8.

ESC-03Outcome carry reconciliation

Required property

For each outcome, currentCarryTotal equals effective inherited unresolved principal plus unresolved local deposits. Effective inherited principal subtracts immediate-parent direct claims and becomes zero for an inherited losing outcome after finalization.

Example: A child snapshots 7 Yes REP, the parent directly claims 2 REP, and the child receives a new unresolved 2 REP Yes deposit. Its current Yes carry is (7 - 2) + 2 = 7 REP.

ESC-04Stable deposit identifiers

Required property

An ordinary game's stable deposit identifier is its local deposit index. A continuation game derives the identifier from its own address, outcome, and local index, so two different continuation deposits cannot share a carry or nullifier key merely because their local indexes match.

Example: Deposit zero on Yes in a child game and deposit zero on Yes in its grandchild produce different stable identifiers.

ESC-05Single-use claims per branch

Required property

Along any single root-to-descendant fork path, each local or inherited deposit may be claimed, settled, refunded, or exported at most once. Child nullifiers are branch-local, but a direct ancestor claim invalidates the matching proof in every descendant and reduces their effective inherited principal. Otherwise, selected sibling branches maintain separate claim authorization.

Example: Consuming a carried proof in a Yes grandchild prevents replay farther down that branch while a sibling remains independent. If the deposit was instead claimed directly from their ancestor, both descendants reject it.

ESC-06Aggregate export accounting

Required property

Aggregate unresolved export clears the exporting vault's three outcome totals, unresolved counter, and parent escrow exactly once. It retains the deposit rows and carry commitment solely as immutable proof material for selected children.

Example: After Alice exports her aggregate claim, her parent escrow is zero even though her historical deposit row remains available to prove a child claim.

ESC-07Authenticated carried winner payout

Required property

A carried claim must authenticate an unconsumed proof for the final winning outcome. The proof fixes the depositor who receives the normal winning payout from aggregate game backing, even when another account relays the transaction.

Example: Bob may relay Alice's valid winning proof, but the contract pays Alice. A losing proof cannot consume backing, and reward math may make a winning payout greater than its principal.

ESC-08Game REP settlement conservation

Required property

Every REP unit held for a game is accounted for exactly once as winning principal, reward funding, losing principal, unsettled residual, or REP swept back to the pool. Settlement cannot create an additional REP claim.

Example: Paying winners and sweeping the final residual reduces the game balance to zero without total payouts exceeding the REP previously held.

ESC-09Terminal game outcomes

Required property

Once resolution or non-decision closes a game path, later deposits cannot reopen or change that terminal result.

Example: After Yes becomes final, a later attempt to deposit on No reverts rather than changing the winner.

ESC-10Ancestor claim replay protection

Required property

If a deposit is claimed directly from an ancestor during an own fork, every existing or later descendant treats the corresponding proof as spent even if that descendant has not written its own nullifier.

Example: Claiming deposit 4 from the parent blocks proof 4 in an already-created child and in a grandchild created later.

ESC-11Residual sweep preconditions

Required property

Residual REP cannot be swept until effective unresolved principal is zero for every outcome and totalEscrowedRep is zero. Inherited losing principal retires at finalization without a proof; winning inherited proofs and every local unresolved deposit still require their applicable terminal transition.

Example: After Yes finalizes, an unclaimed inherited No leaf does not block sweeping. An unclaimed inherited Yes proof, an unsettled local deposit, or a live vault escrow record still does.

ESC-12Pool and continuation payout agreement

Required property

When a universe forks on a pool's question, each child pool and its continuation game use that child's Invalid, Yes, or No branch as the final pool-question outcome. Once a pool inherits that fixed outcome, new local escalation deposits and every later fork transition revert, whether the new universe fork uses the same question or another one. Deposit withdrawal reverts unless the pool and game report the same outcome.

Example: A Yes child created by a fork on the pool question pays carried Yes deposits even if copied game balances favored No. It rejects new local escalation REP before escrow, so a later local non-decision cannot lock vault redemption. A later matching or unrelated universe fork leaves the stored SystemState.Operational and fixed Yes outcome unchanged, and eligible share, vault REP, and carried-proof redemption paths remain available, while universe-fork guards still freeze normal operating calls.

ESC-13Non-decision threshold arithmetic

Required property

For a positive fork threshold F, non-decision requires ceil(F / 2) REP on two outcomes. Therefore the two threshold balances total at least F, while one wei less on both outcomes totals strictly less than F.

Example: If F = 5, non-decision requires 3 REP on two outcomes, so the two balances hold 6 REP; balances of 2 and 2 remain below the 5 REP fork threshold.

REP/ETH Oracle Operations

Accepted oracle design properties—not security findings. Statoblast uses profitable correction, not operation-value collateralization. Report liquidity is intentionally not required to equal or bound the value of withdrawals, liquidations, allowance changes, pool assets, or cumulative operations that use an accepted price. The deployment assumption is ORACLE-A1, cataloged here as ORA-10: at least one adequately capitalized participant takes every profitable correction and obtains inclusion before settlement.

The protocol also makes no bounded-liveness claim for a pending sponsor lane. Every valid dispute restarts settlement, incurs transaction execution, and must fund the contract-specified replacement position. Under ordinary non-dust parameters, protocol fees and the required position also accumulate; before the escalation halt, integer flooring can leave dust-sized rounds unchanged. A participant willing and able to keep submitting and funding disputes may therefore delay unrelated users without a coordinator-level deadline. This paid, capital-unbounded pause is intentional and is not a violation of a Zoltar liveness invariant.

Security review should verify the correction-profit calculation, report accounting, dispute access, and the stated inclusion assumption. A concrete bypass of the required position or fee, capital reuse, invalid deadline transition, or cache-conformance failure remains a finding. The mere absence of a report-notional bound or absolute pending-report duration does not. See the normative review classification.

ORA-01Authorized settlement callbacks

Required property

Only the configured OpenOracle may supply a settlement callback, and its report identifier must equal the coordinator's pending report.

Example: A callback from another contract or for an older report ID cannot update the cached REP/ETH price.

ORA-02REP-per-ETH price direction

Required property

An accepted price is positive REP per ETH: amount2 REP × 1e18 / amount1 WETH. Higher values require more REP for the same ETH obligation.

Example: A report of 200 REP for 2 WETH stores 100 REP per ETH, not 0.01 ETH per REP.

ORA-03Five-minute price validity

Required property

A cached price is usable only while nonzero and strictly younger than the five-minute validity window.

Example: A price settled exactly five minutes ago is stale; one settled four minutes and 59 seconds ago remains usable.

ORA-04Single-use staged operations

Required property

Every staged operation has one immutable identifier. Once execution is attempted with a usable price, success or a caught failure consumes that identifier, emits the result, and prevents a retry. An uncaught transaction revert instead rolls back the entire attempt.

Example: A pool-level withdrawal rejection is caught and emitted as failed, after which the same operation ID cannot be executed again.

ORA-05Staged operation targets

Required property

Withdrawals and allowance changes target the initiating vault; liquidations target another vault and fail when the protected snapshot becomes stale.

Example: Alice can stage her own REP withdrawal, but a staged liquidation names Bob and fails if Bob changes his allowance before execution.

ORA-06Consumed execution failures

Required property

An expired operation, a liquidation with a stale target snapshot, a withdrawal that would move zero REP, or a liquidation inside the configured minimum price distance is consumed with an observable failure result rather than remaining executable forever.

Example: If an earlier withdrawal empties a vault, its second queued withdrawal is consumed as a zero-effect failure rather than retried after every price update.

ORA-08Dispute and settlement boundary

Required property

The settlement deadline is exclusive: disputes require the current clock to be strictly before the deadline, while settlement is available at and after it.

Example: At timestamp deadline, a new dispute is rejected and settlement is allowed.

ORA-10Active arbitrager assumption

Required deployment assumption

At least one independent, rational, adequately capitalized participant continuously monitors pending reports, acts whenever correction is profitable under the configured economics, and can obtain dispute inclusion before settlement.

Example: When a false report can profitably be corrected, at least one funded watcher notices it and gets a correcting dispute included before the deadline.

Truth Auctions

AUC-01Bid admission

Required property

Bids are accepted only during the one-week window, at a supported tick whose computed ETH-per-REP price is positive, and at or above the auction's minimum bid size.

Example: A bid submitted one second after the one-week window or below the minimum bid size reverts without being recorded.

AUC-02Auction caps

Required property

Final retained ETH never exceeds the ETH raise cap, and total purchased REP never exceeds the REP sale cap.

Example: If bids offer 12 ETH against a 10 ETH cap, finalization retains at most 10 ETH and refunds the rest.

AUC-03Single-use bid settlement

Required property

Each bid is settled or refunded at most once; claimed state is set before an external ETH refund.

Example: A bidder whose refund callback reenters cannot withdraw the same bid a second time because it is already marked claimed.

AUC-04Claim-order independence

Required property

Cumulative allocation math makes per-bid REP, refund, and security-bond allowance results independent of post-finalization claim order.

Example: Alice claiming before Bob gives each vault the same REP, ETH refund, and allowance as Bob claiming before Alice.

AUC-05Allocation and refund reconciliation

Required property

A zero-demand auction records zero purchased REP. Otherwise, the sum of all winning-bid REP allocations equals the stored aggregate purchase, and each bid's unretained ETH remains refundable.

Example: If finalization stores 30 purchased REP, all winning claims together receive exactly 30 REP and every unused bid wei is returned.

AUC-06Bidder-vault credits

Required property

A bid claim credits purchased REP, pool ownership, and its fixed-position share of the complete unmigrated allowance to the bid's recorded vault. These credits add to rather than replace that vault's migrated position, and cumulative allocation keeps allowance rounding independent of claim order. A winning dust bid still receives a positive fixed-position allowance share when its REP allocation rounds to zero.

Example: A vault with migrated ownership keeps it when claiming auction REP; the claim adds the ownership and deterministic allowance share assigned to that winning bid. If a dust bid's REP share is zero but its allowance share is positive, claiming that bid alone still credits the allowance.

AUC-07Uniform weak-demand allocation

Required property

Under AUCTION-A1, qualifying ETH is retained bid ETH offered at or above the cap-implied qualification threshold. The threshold is not an execution-price floor. Qualifying bidders collectively receive maxRepBeingSold in proportion to that ETH at the aggregate effective price underfundedWinningEth / maxRepBeingSold. Per-bid cumulative floors then assign indivisible atomic units, so a dust winner can round to zero REP without changing the aggregate price. With no qualifying ETH, every bid refunds.

Example: If Alice supplies 60% and Bob 40% of qualifying ETH, they receive 60% and 40% of the complete REP sale cap subject to deterministic atomic-unit rounding.

AUC-08Forced-ETH-resistant finalization

Required property

Auction finalization succeeds regardless of unsolicited ETH already present in the child pool or forker.

Example: One wei forced into the child before finalization remains surplus and does not change protocol-accounted collateral.

AUC-09Bounded bid settlement

Required property

After the auction deadline, value-free finalization succeeds using migration-routed collateral plus retained auction ETH. Qualifying bids settle for REP, non-qualifying bids refund, and nonzero finalizer ETH reverts.

Example: For a 10 ETH target with 6 ETH migrated and 3 ETH retained from bids, the child activates with 9 ETH of accounted collateral and every bid can then settle.

AUC-10Persistent tick bid history

Required property

Bid cumulative ETH remains append-only for a tick even when the active AVL node is deleted and later recreated. Refunded history is subtracted exactly once, so every later accepted bid retains a valid allocation or refund path.

Example: Deleting an empty price tick and later bidding at that price continues cumulative ETH after the old history instead of making the new bid unclaimable.

Lifecycle, Liveness, and External Calls

LIFE-01Pool state transitions

Required property

Pool state topology permits only Operational → PoolForked for a parent and ForkMigration → ForkTruthAuction → Operational for a child.

Example: A child cannot skip directly from ForkMigration to Operational while repair auction work remains required.

LIFE-02Permissionless transition liveness

Required property

Once a resolution, migration, auction-completion, or withdrawal function's documented semantic preconditions hold, dust, unsolicited balances, empty collections, or earlier permissionless calls cannot permanently prevent some caller from completing it.

Example: Forced ETH and an empty losing-bid list do not prevent a caller from finalizing an otherwise complete truth auction.

LIFE-03Atomic failure behavior

Required property

An uncaught revert rolls back every state mutation and transfer in the transition; deliberate consumed failures emit an explicit result and cannot be retried.

Example: If a child migration reverts after an attempted token transfer, neither the transfer nor its accounting update remains committed.

LIFE-04Deadline equality rules

Required property

Every deadline assigns equality to one documented side of the boundary: migration remains open at equality; auction bidding and public pool finalization are both closed at equality, and finalization opens immediately afterward; oracle disputes are closed and settlement is open at equality; staged operations expire only after equality; and an escalation result is final only after its end timestamp.

Example: Exactly at an auction deadline, both a bid and public pool finalization revert; one second later, finalization succeeds.

LIFE-05Bounded transition work

Required property

No mandatory transition loops over an attacker-unbounded history in one transaction; callers use bounded pages, fixed outcome sets, proofs, or balanced-tree traversal.

Example: Settling one carried deposit verifies its bounded proof instead of iterating over every deposit ever made in its ancestors.

EXT-01Token behavior assumptions

Required property

REP, child REP, and WETH obey the exact transfer, return-value, decimal, and callback behavior assumed by pool and oracle accounting.

Example: REP transfer returns and moves exactly the requested atomic units rather than charging a fee that leaves pool accounting overstated.

EXT-02Callback-safe accounting

Required property

External ETH or token callbacks observe effects already committed for that action, and a failed transfer reverts without leaving partial accounting.

Example: A fee recipient's fallback observes its fee debt already cleared, so reentry cannot redeem the same debt twice.

EXT-03ERC-1155 callback safety

Required property

ERC-1155 receiver callbacks cannot mint beyond pool capacity, alter the amount minted, or reenter the same accounting effect twice.

Example: A receiver callback during complete-set minting cannot call back into the pool and reuse the same ETH capacity for a second mint.

EXT-04Same-block deadline ordering

Required property

At a deadline timestamp, mutually exclusive before-deadline and after-deadline actions cannot both succeed. Explicit comparison operators assign equality to one phase, and transaction ordering within the block cannot change that assignment.

Example: At the OpenOracle settlement deadline, ordering a dispute before settlement in the block still cannot make the dispute valid.

EXT-05Recursive fork gas bound

Required property

Origin registration, inherited-fork detection during child construction, and direct-claim replay checks must not traverse universe or pool ancestry.

Example: At lineage depths 1 and 32, a replay query for the same global deposit id performs the same lineage-registry and claimed-id lookups rather than 1 or 32 parent calls.

Verification Obligations

A change should name the invariant identifiers it can affect. Tests should then attempt to falsify those statements across the complete transaction sequence, including calls immediately before and after the state transition.

Family Existing coverage Required additions
Authority and deployment Factory, CREATE2, fake-parent, interface, and storage-layout regression tests. Manifest-to-runtime bytecode and constructor-wiring verification.
Universes and REP zoltar.test.ts and fork/migration invariant scenarios. Stateful supply conservation across several recursive forks and selected child sets.
Pool, shares, and vaults vaultAccounting.test.ts and forkMigration.test.ts, plus peripheralsInvariant.test.ts. Together, these cover forced balances, prefunded migration proxies, zero-supply bootstrap, unequal child outcome supplies, and positive-output mints. Caller-selectable mint slippage protection and broader stateful vault/share accounting sequences.
Escalation and carry escalationGame.test.ts and escalationMigration.test.ts, plus direct and recursive fixed-outcome fork coverage in forkMigration.test.ts and even/odd non-decision boundaries in escalationGameForkThreshold.test.ts. The escalation-game suite also compares direct-claim replay gas at lineage depths 1 and 32. Extend depth-independent gas regressions whenever a new lineage-sensitive settlement or deployment path is added.
Oracle priceOracleSecurity.test.ts and openOracleDispute.test.ts, including exact-deadline settlement exclusivity, dynamic minimum report sizing, sponsor exclusivity, manual overflow execution, and staged-operation invariant tests. Validation that the configured multiplier is economically sufficient under deployment-specific gas and inclusion assumptions.
Auctions auction.test.ts, truthAuction.test.ts, including value-free weak-demand finalization, forced-balance isolation, underfunded-threshold qualification, uniform pricing, claim-order, and tick-math coverage, plus bid-history preservation across repeated tick deletion and recreation. Stateful bidder/order fuzzing across weak-demand finalization and post-finalization refunds.
Cross-contract lifecycle peripheralsInvariant.test.ts and deadline scenario tests. Stateful action-sequence fuzzing with dust and adversarial ordering across repeated forks.