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 Protocol Security Model for assumptions A01–A28. Funded and underfunded clearing are explained in the Truth Auction clearing guide; oracle notional and residual-loss analysis are explained in OpenOracle Integration.
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.
No invariants match the selected filters.
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. |
| 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. |
| Automated tooling guard | Release, deployment, or CI tooling rejects a mismatched artifact, address, or runtime-code identity before it is accepted. | Keep the check deterministic, run it in the documented release path, and test both matching and mismatched inputs. |
Invariant identifiers are stable review labels. They are grouped by authority, universe, question, asset, share, vault, fork, escalation, oracle, auction, lifecycle, and observability 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.
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
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
⌈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 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 haircut, and receives 40 REP of migration credit.
UNI-04Deterministic child universe IDs
Required property
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
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
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
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
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.
UNI-09Child REP supply coherence
Required property
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.
Questions and answer classification
QST-01Question registry and classifier coherence
Required property
Malformed.
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.
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.
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.
Every successful external call should reconcile raw ETH into named liabilities or an explicit surplus bucket. All equation terms are denominated in attoETH; raw balance alone must not define collateral.
BAL-01ETH conservation
Required property
raw ETH = tracked collateral + unallocated fee reserve + total claimable vault fees + 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
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 and backing
Required property
Example: If current oracle-priced capacity is 10 ETH, a mint that would raise tracked collateral from 9 ETH to 11 ETH reverts even if the raw balance contains surplus ETH. A mint within that 10 ETH capacity also reverts if unresolved escalation has moved too much REP out of the pool to cover the resulting active open interest. A later REP price change can lower capacity or backing below the checked boundary without changing existing open interest or ownership records.
BAL-04REP coverage boundaries
Required property
Example: A receiver approved at 12,000 BPS must retain 1.2× the upward-rounded associated-REP requirement and 1.2× the upward-rounded free-REP requirement after accepting live debt. Passing only one branch is insufficient.
BAL-05REP backing units conversion consistency
Required property
uint256.Example: Depositing REP and immediately converting the resulting REP backing units back to REP uses the same denominator rather than a stale pre-deposit balance.
BAL-06Fee liability accounting
Required property
Example: Assigning 3 attoETH of reserve to a vault decreases unallocated reserve by 3 and increases that vault's claimable fees by 3, without creating a second claim.
BAL-07Fee reserve protection
Required property
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.
BAL-08Aggregate pool-ledger coherence
Required property
totalClaimableVaultFeesAttoEth equals summed unpaid vault fees. In Operational, fee-eligible capacity ownership equals summed live vault capacity ownership plus sold truth-auction ownership awaiting claim. Uncheckpointed capacity ownership covers fee-eligible ownership not yet reconciled to the current global index, including an unclaimed auction allocation after the index advances. During ForkMigration, configured migrated capacity ownerships remain pending outside those pool aggregates. A PoolForked
parent retains its fork-time total and fee-eligible snapshots as individual vaults migrate. After a positive-purchase truth-auction activation, total capacity ownership equals fee-eligible capacity ownership, including the outstanding unclaimed auction allocation in both aggregates. If the auction purchases zero REP, the unmigrated remainder remains explicit unassigned capacity but stays outside fee eligibility. At finalization and after every claim, every capacity unit counted by the child belongs either to a real vault or to that nonwithdrawable unassigned position. The
auction settlement specification
defines that zero-purchase allocation rule. Per-vault remainder carries make ordinary fee claims independent of checkpoint frequency and claim order. At a terminal fork, after all capacity behind the final index has been checkpointed, the only unreconciled whole-attoETH reserve is cumulative division residue: it is less than one attoETH per independently rounded fee-entitlement ledger or global fee-index denominator epoch. Here N counts each vault entitlement ledger, any separately checkpointed unassigned auction entitlement, and each denominator epoch whose global remainder is cleared when fee-eligible capacity changes; repeated checkpoints within the same ledger and epoch carry their remainder and do not increase N. The total is therefore strictly less than N attoETH. Because the configurable vault floor and auction settlement can create no protocol-wide small bound on N, the terminal recovery path is retained and releases that reserve only after uncheckpointedFeeEligibleCapacityOwnershipAttoRep reaches zero.
Example: Migrating one of two vaults that each own 3 REP of capacity leaves the parent's frozen 6 REP total unchanged and records 3 REP as unassigned in the child. With purchased REP, finalization adds those 3 REP of sold ownership to fee eligibility immediately, and later claims only transfer the position to bidder vaults. With zero purchased REP, the same 3 REP remains system-owned and ineligible.
VAULT-01Dispute-staked REP isolation
Required property
Example: A vault initially attributed 20 REP that dispute-stakes 5 REP is left with 15 REP of vault backing plus a separate 5 REP claim. It cannot make an ordinary withdrawal while that escrow remains; ordinary vault migration moves only the 15 REP backing, while the dispute-staked REP claim follows its separate migration path.
VAULT-02Liquidation conservation and freshness
Required property
Example: If the target or receiver changes after staging, execution may fail safely and release the full reservation. The operator receives no ownership merely for submitting the transaction.
VAULT-04Escalation claims are non-transferable and migration-neutral
Required property
Example: Moving half a vault's capacity ownership leaves every escalation claim unchanged, and locking that claim cannot increase the OI routed to any child.
VAULT-03Vault registry coherence
Required property
_registerVault, including a public fee checkpoint for an empty address, can append it. Pagination is newest-registered first; later activity and full exit do not reorder or remove an entry. Consumers read current vault and escalation state to decide which registered vaults to display.Example: After a vault has fully exited and its REP backing, capacity ownership, claimable fees, escalation stake, bad debt, and open interest are all zero, its address remains in registry pagination. A UI can filter the empty position without losing historical discovery.
Forks and child isolation
FORK-01Parent pool finality
Required property
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
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
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
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
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. This pool-local boundary does not limit Zoltar.deployChild, addRepToMigrationBalance, or splitMigrationRep; those Zoltar operations follow their own fork identity and balance guards without this timestamp check.Example: Vault migration succeeds exactly at the eight-week deadline and reverts one second later.
FORK-06Child deployment identity
Required property
Example: On the external-universe path, the forker first requires the source to be authorized by its declared share token without treating that check as factory registration. The configured canonical factory installs the parent's share token, pool question, and multiplier in the child; the post-deployment guard then checks deployed and unique auction assignment plus parent, universe, factory, forker, and auction relationships before linking it.
FORK-07Single-use non-escrowed vault migration
Required property
Example: After Alice migrates her non-escrowed vault accounting to the Yes child, a second migration call cannot credit the same parent REP backing units to the No child.
FORK-08One-time aggregate continuation backing
Required property
sourcePrincipalAtForkAttoRep - ⌊sourcePrincipalAtForkAttoRep / 5⌋, the rounded-up 80% minimum, and the live balance must cover the unexported remainder after valid direct pre-resume claims. sourcePrincipalAtForkAttoRep is the raw aggregate stored by the fork snapshot before effective direct-claim deductions.
Example: Creating the Yes child installs its snapshot and aggregate backing before Alice acts. Alice may later clear her unresolved parent escalation-deposit accounting, but that cleanup neither funds the child nor enables or disables her winning proof.
FORK-09Cumulative child collateral
Required property
Example: If several calls collectively migrate R child REP, their collateral target is ⌈fork collateral × R / denominator⌉, independent of how that same R is partitioned. The denominator is vaultRepAtForkAttoRep for an own fork and auctionableAttoRepAtFork otherwise.
FORK-10Share migration integrity
Required property
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
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
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
totalDisputeStakedAttoRep equals effective live vault-denominated escrow plus effective aggregate continuation backing in forkCarryDisputeStakedAttoRep. Continuation backing is not assigned to child-vault health or migration power, but it must enter the aggregate before the Truth Auction so physically held REP cannot escape the repair haircut. Auction retention floors the aggregate total and the continuation bucket independently; do not reconstruct either aggregate by summing independently rounded vault views.Example: If vault-denominated escrow contributes 4 and 6 REP and an external-fork continuation carries 12 REP of aggregate proof backing, the total is 22 REP, represented as 22 × 10^18 attoREP in totalDisputeStakedAttoRep, before the auction. A 75% retention records ⌊22 × 75%⌋ = 16 total effective REP and ⌊12 × 75%⌋ = 9 aggregate continuation REP. This makes the carried claims absorb the same repair loss without pretending that their backing belongs to a particular child vault.
ESC-02Local unresolved REP reconciliation
Required property
totalLocalUnresolvedAttoRep 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
currentCarryTotalAttoRep 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
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
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
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
Example: Bob may relay Alice's valid winning proof, but the payout still goes entirely to Alice as the committed depositor. 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
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
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
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
forkCarryDisputeStakedAttoRep; after that retirement, no local dispute stake or vault escrow may remain in totalDisputeStakedAttoRep. Inherited losing principal retires at finalization without a proof; winning inherited proofs and every local unresolved deposit still require their applicable terminal transition. Ordinary-game residual returns to the pool, while fork-continuation residual is burned and cannot accrue to child-local backing units.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
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 dispute-staked 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 and live start-bond arithmetic
Required property
F, non-decision requires ⌈F / 2⌉ REP on two outcomes. Therefore the two threshold balances total at least F, while one attoREP less on both outcomes totals strictly less than F. At pool construction, the configured start bond is max(1 REP, live universe theoretical REP supply / 10,000,000), and a new origin requires the live non-decision threshold to exceed it. If an existing pool's live threshold later falls to or below that configured bond, ordinary game deployment clamps the live start bond to nonDecisionThresholdAttoRep - 1, provided the threshold exceeds one attoREP.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.
ESC-14Carry commitment structural integrity
Required property
ESC-03.
Example: Three Yes leaves occupy the height-zero and height-one peaks; bagging those two peaks reproduces the exported Yes root before and after one inherited proof is consumed.
REP/ETH oracle operations
Security assumptions: A18 independent correction incentive, A19 observable correctable price, and A06 lifecycle executors.
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, capacity ownership changes, pool assets, or cumulative operations that use an accepted price.
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.
ORA-01Authorized settlement callbacks
Required property
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
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-03Oracle price validity
Required property
Example: On mainnet, a price whose final report reached settlement eligibility exactly five minutes ago is stale; one that reached it four minutes and 59 seconds ago remains usable.
ORA-04Single-use staged operations
Required property
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
Example: Alice can stage her own REP withdrawal. A liquidation operator can target Bob, but its receiver cannot be Bob; execution fails if Bob changes his REP backing units or capacity ownership after staging.
ORA-06Consumed execution failures
Required property
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-07Staged-operation queue and index bijection
Required property
pendingOperationSlotId is zero for an empty queue or equals its head.
Example: Settling four queued operations removes those four IDs from both indexes, leaves an overflow operation active for manual execution, and does not reuse any consumed ID.
ORA-08Dispute and settlement boundary
Required property
Example: At timestamp deadline, a new dispute is rejected and settlement is allowed.
ORA-09Oracle balance-domain boundary
Required property
Example: REP transferred directly to the coordinator remains there, while REP deposited into OpenOracle for the coordinator is swept with the report proceeds to the current sponsor and leaves only OpenOracle's balance sentinel.
Truth Auctions
AUC-01Bid admission
Required property
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
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
withdrawPendingEthRefund clears the caller's credit before its only external call, and a rejected transfer reverts the clear.Example: A reverting bidder cannot block settlement or withdraw another bidder's credit. Its own failed pull preserves the complete balance for a later authorized retry.
AUC-04Claim-order independence
Required property
Example: Alice claiming before Bob gives each vault the same REP, ETH refund, and capacity ownership as Bob claiming before Alice.
AUC-05Allocation and refund reconciliation
Required property
Example: If finalization stores 30 purchased REP, all winning claims together receive exactly 30 REP and every unretained attoETH is refunded.
AUC-06Bidder-vault credits
Required property
Example: A vault with migrated REP backing units keeps them when settling a winning auction bid. A current-generation claim moves the bid's backing units, deterministic capacity share, proportional bad debt, and accrued fees into that vault while leaving every pool aggregate unchanged. If the generation has expired, the same claim moves the backing units, capacity share, and fees but assigns no old debt. If a dust bid's REP share is zero but its capacity ownership share is positive, claiming that bid alone still credits the capacity ownership.
AUC-07Uniform weak-demand allocation
Required property
maxAttoRepBeingSold in proportion to that ETH at the aggregate effective price underfundedWinningAttoEth / maxAttoRepBeingSold. Per-bid cumulative floors then assign indivisible attoETH and attoREP, 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 attoREP rounding.
AUC-08Forced-ETH-resistant finalization
Required property
Example: One attoETH forced into the child before finalization remains surplus and does not change protocol-accounted collateral.
AUC-09Bounded bid settlement
Required property
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
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.
AUC-11Auction tree and public-model equivalence
Required property
AUC-12. Historical insertion and refund-prefix obligations are owned by AUC-10.
Example: Before finalization, an independent descending-tick scan returns the same clearing result as the contract. After a winner settles, its bid is marked claimed and any refund moves to pull credit, while the final clearing page and result remain unchanged.
AUC-12Auction ETH liability conservation
Required property
pendingEthRefundsAttoEth and explicit surplus. After finalization, the remaining balance equals refunds still attached to unclaimed bids plus credited pendingEthRefundsAttoEth and explicit surplus. Settling a refund moves value between those two liabilities without transferring ETH; only an authorized pull reduces the balance. Per-bid settlement partitions and aggregate REP allocation are owned by AUC-05.
Example: Settling a 2 ETH losing bid removes it from active clearing and adds a 2 ETH bidder credit, leaving raw auction ETH unchanged until that bidder pulls it.
Lifecycle, liveness, observability, and external calls
Security assumptions: A02 viable operating costs, A16 timely inclusion, A06 lifecycle executors, and A26 Ethereum execution.
LIFE-01Pool state transitions
Required property
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
Example: Forced ETH and an empty losing-bid list do not prevent a caller from finalizing an otherwise complete Truth Auction.
The named LIFE-02 fixed-point stateful regressions combine empty zero-demand auctions, unsolicited ETH, repeated migration calls, shuffled partial migration, and bounded continuation progress, then require a reachable terminal child state with tracked accounting unchanged by the forced balance. The wider lifecycle audit also covers empty games and collections, repeated claims, delayed oracle operations, and recovery after failed callbacks. No permanent blocker was identified in those cases.
LIFE-03Atomic failure behavior
Required property
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
Example: Exactly at an auction deadline, a bid reverts and public pool finalization succeeds; transaction ordering cannot reopen bidding.
LIFE-05Bounded transition work
Required property
Example: Settling one carried deposit verifies its bounded proof instead of iterating over every deposit ever made in its ancestors.
OBS-01Event-state replay equivalence
Required property
Example: Replaying seeded pool and vault operations matches their accounting storage, while replaying a deployed parent deposit, fork snapshot, and child carry checkpoint matches the child's roots, peaks, leaf counts, unresolved totals, and nullifier roots.
EXT-01Genesis token behavior boundary
Required property
GenesisReputationToken for issuance mechanics and on Uniswap's published Sepolia WETH, verified only by runtime-code hash. Burn-sink inaccessibility remains an external assumption on both networks.
Example: Genesis REP transfer returns and moves exactly the requested attoREP rather than charging a fee that leaves pool accounting overstated; child REP supply remains bounded by its contract-enforced theoretical ceiling.
EXT-02Callback-safe accounting
Required property
Example: A fee recipient's fallback observes its claimable fees already cleared, so reentry cannot redeem the same claimable fees twice.
EXT-03ERC-1155 callback safety
Required property
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
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
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.