This repository is a training lab, not production financial software.

For each supported token:

sum(user internal claims) <= ERC20.balanceOf(pool)

Deposits credit observed assets, failed withdrawals preserve claims atomically, and privileged withdrawal / settlement operators are explicit trust boundaries.

The hardened EIP-712 flow binds user, token, recipient, amount, nonce, deadline, chain ID, and verifying contract.

A successful signed authorization consumes exactly one nonce. Failed downstream execution rolls that state change back.

The hardened queue preserves global liveness while retaining failed user claims for retry.

Key properties include monotonic bounded cursor movement, terminal state for attempted entries, pending state for future entries, retryability of failed requests, and conservation of deposits across outstanding claims plus successful payouts.

A strict batch nonce provides ordering and replay protection. It does not prove that credits are backed, P/L is economically valid, or off-chain trades occurred.

The hardened lab model therefore requires:

• exact sequential batch nonce;
• sequencer authorization;
• one-time asset-backed deposit receipts;
• zero-sum P/L in the closed settlement model.

That zero-sum rule is intentionally not presented as a universal perp formula. Production systems must explicitly model fees, funding, liquidation flows, insurance, LP / market-maker counterparties, and bad debt.

PerpRisk.sol models a linear perpetual:

P/L = signed size × price change / entry price
equity = collateral + P/L
margin = notional × configured margin rate

Positive signed size is long; negative signed size is short.

1. Opening collateral must meet initial margin.
2. Maintenance margin is lower than initial margin by constructor configuration.
3. Collateral removal must leave resulting equity at or above initial margin.
4. In this lab, liquidation becomes eligible at equity <= maintenance margin.
5. Equal-and-opposite positions at the same entry and mark have equal-and-opposite price P/L.
6. P/L is zero at entry price.
7. Position notional and price inputs are bounded when opened.
8. Mark prices are bounded inside the pure risk math before multiplication.

The lab caps:

abs(sizeUsd) <= 1e36
price <= 1e30

These bounds keep size × priceDelta safely inside signed 256-bit arithmetic for the lab's 18-decimal USD representation.

Margin requirements are also bounded by notional and a rate no greater than 100%, so conversions used when comparing unsigned margin requirements with signed equity are safe under these bounds.

The lab uses:

equity <= maintenance margin

as the liquidation threshold.

This is a conservative explicit convention for this project. Different production protocols can differ in exact boundary semantics, fee inclusion, oracle choice, maintenance tiers, or pre-liquidation buffers.

IsolatedMarginBook.liquidate currently closes position risk state only.

It does not yet settle:

• trader residual equity;
• counterparty / LP P&L;
• liquidator rewards;
• liquidation fees;
• protocol fees;
• funding;
• insurance-fund debits;
• bad debt.

Those are intentionally deferred so the next milestone can encode a full conservation equation.

• VulnerablePool.sol: unbacked fee-on-transfer deposit accounting.
• VulnerableWithdrawalManager.sol: signed nonce without replay enforcement.
• VulnerableForcedWithdrawalQueue.sol: FIFO head-of-line blocking.
• VulnerableSettlementVerifier.sol: sequential batches that can still create arbitrary liabilities.

Three independent stateful suites cover Pool accounting, queue liveness, and settlement conservation.

Each verified suite runs:

256 invariant runs
16,384 randomized handler calls
0 handler reverts

The perp risk layer additionally has deterministic boundary tests and two 1,000-run fuzz properties.

Not yet implemented:

• liquidation asset settlement;
• insurance fund / bad debt;
• funding;
• trading / liquidation fees;
• oracle freshness / manipulation checks;
• Base fork state;
• UUPS storage layouts and upgrade authorization;
• formal verification;
• cross-chain message proofs.

Those are subsequent milestones.

The perp-risk module introduces signed linear position accounting.

Security properties:

1. positive size is long and negative size is short;
2. long/short PnL is symmetric for equal and opposite positions;
3. PnL is zero when mark price equals entry price;
4. a position cannot open below initial margin;
5. collateral cannot be removed if resulting equity falls below initial margin;
6. liquidation is allowed only when equity is at or below maintenance margin;
7. exact maintenance-margin equality is treated as liquidatable;
8. extreme notional/price inputs are rejected before state storage and before unsafe multiplication.

IsolatedMarginBook intentionally separates risk eligibility from financial settlement.

Closing a liquidatable position currently changes risk state only. It does not decide who absorbs losses or how remaining collateral is distributed.

The next security boundary is therefore:

liquidation equity >= 0
    => residual collateral allocation + liquidation fee

liquidation equity < 0
    => bad debt
    => insurance fund / explicit loss waterfall

Until that layer exists, the module must not be described as a production liquidation engine.

The clearing-house milestone converts abstract liquidation equity into actual token movements.

For positive liquidation equity:

collateral
=
realized loss paid to counterparty
+
liquidation fee retained as insurance
+
trader residual

The fee is capped by positive equity, so liquidation cannot create a negative trader payout.

For negative equity:

bad debt
=
insurance coverage
+
uncovered bad debt

and:

counterparty payout
=
all trader collateral
+
insurance coverage

The protocol does not fabricate settlement assets to erase a deficit.

Under the stateful harness:

clearing-house ERC-20 balance
=
total open collateral
+
insurance balance

and every minted settlement token remains located in one of:

• clearing house;
• explicit counterparty;
• trader wallets;
• invariant handler during funding setup.

The current model has no debt-resolution path.

Therefore:

uncoveredBadDebt(t + 1) >= uncoveredBadDebt(t)

must hold.

A future ADL / recapitalization mechanism must make any decrease explicit and separately conserved.

The fixed counterparty address represents the winning-side/system settlement recipient. That is a deliberate simplification: a production matching engine must prove which counterparties are owed realized P/L rather than routing all losses to one address.

Funding is modeled as a market-level transfer between the long and short sides.

Security properties:

1. market-level funding paid equals market-level funding received;
2. a position only accrues funding after its own checkpoint;
3. settling twice without additional time/rate movement produces zero new funding;
4. a position opened after historical accrual starts at the current cumulative index;
5. one-sided markets do not accrue funding;
6. positive rate means longs pay shorts; negative rate means shorts pay longs;
7. rate magnitude is bounded;
8. unequal open interest changes per-size receiving rates but does not create market-level value.

The current model tracks funding accounting only. It does not yet debit or credit the ERC-20-backed clearing-house collateral balances.

That integration is a separate security boundary because funding settlement against collateral can itself trigger margin changes or liquidation.

OracleGuard treats price freshness as part of the liquidation authorization path.

Required conditions:

price > 0
updatedAt > 0
updatedAt <= block.timestamp
block.timestamp - updatedAt <= maxAge

If any condition fails, entry/equity/liquidation logic must revert before using the price.

A mathematically correct maintenance-margin formula is still unsafe if the mark price is stale, malformed, or timestamped in the future.

The oracle adapter therefore sits before risk math rather than being treated as a UI/data-quality concern.

The lab validates freshness and timestamp sanity, but it does not prove the source's economic correctness.

Still external to the model:

• source aggregation;
• signer / validator quorum;
• deviation checks between sources;
• sequencer uptime;
• confidence intervals;
• market-specific circuit breakers.

Those are future hardening layers.

Upgradeability adds a privileged code-replacement path, so both authorization and storage compatibility are security-critical.

Only the configured proxy owner may authorize a UUPS implementation change.

The implementation itself cannot be used as an upgrade execution context because OpenZeppelin's UUPS logic requires proxy delegation.

The implementation instance is locked during construction.

The proxy receives initialization calldata during ERC-1967 deployment, preventing a window where an uninitialized proxy could be claimed by a third party.

A safe implementation upgrade must preserve every previously allocated storage location.

Safe:

V1:
slot 0 owner
slot 1 collateralFactor
slot 2 totalLiabilities
slot 3 mapping

V2:
same V1 slots
+ appended fields

Unsafe:

slot 0 NEW FIELD
slot 1 old owner
slot 2 old collateralFactor
...

The unsafe case does not merely produce wrong UI values. It can:

• reinterpret financial state;
• make existing mapping entries unreachable;
• corrupt access-control state;
• lock the legitimate administrator out of recovery.

A proposed implementation must expose the expected ERC-1822/UUPS interface. A non-UUPS implementation is rejected rather than silently disabling future upgradeability.

This milestone intentionally uses a single owner as the upgrade authority.

A production protocol should typically place that authority behind stronger governance such as a multisig, role system, and/or timelock. Delayed upgrade execution is the next governance layer for this lab.

Upgrade authorization is now modeled as a multi-stage process rather than a single privileged EOA call.

Security properties:

1. only the proposer role may schedule an upgrade;
2. only the designated executor may execute it;
3. execution cannot occur before the configured minimum delay;
4. unscheduled operations cannot execute;
5. scheduled operations can be cancelled by an explicitly granted canceller role;
6. the proxy itself recognizes only the timelock as upgrade owner;
7. V2 reinitialization can be bundled atomically with the implementation change.

The timelock guarantees when an authorized code change can happen.

It does not guarantee that the proposed implementation is:

• storage compatible;
• economically safe;
• bug free;
• correctly initialized.

Therefore upgrade safety requires both:

governance controls
+
implementation validation / storage-layout review

The test suite deliberately schedules and executes a storage-incompatible implementation to prove this distinction.

Mocks are useful for adversarial behavior, but they cannot prove compatibility with a live deployed token.

The fork suite therefore executes the hardened Pool against canonical native Base USDC.

Properties checked on live fork state:

1. chain identity is Base Mainnet (8453);
2. the configured USDC address contains deployed code;
3. token precision is 6 decimals;
4. requested standard-USDC deposit equals actual received balance delta;
5. internal liabilities equal USDC held by Pool after deposit;
6. withdrawal reduces liabilities and real token backing by the same amount.

The test seeds USDC to a synthetic account with Foundry's fork-local deal cheatcode.

This does not claim that the synthetic account owns those assets on real Base. It changes only the ephemeral fork state so the test can exercise the live token implementation deterministically.

The public Base RPC is an external dependency of this integration gate.

A production CI setup could pin a specific block and use a dedicated authenticated RPC provider for stronger reproducibility and availability. Local unit/fuzz/invariant tests remain independent of RPC availability.

OperationalSafetyVault treats incident response as an on-chain state machine rather than an off-chain convention.

Normal custody operation:

• deposits;
• sequencer-backed internal state changes;
• withdrawals.

The sequencer may not create liabilities above actual token backing.

Security objective:

stop new risk
while
preserving solvent user exits

Once ExitOnly is active:

• deposits are blocked;
• sequencer state changes are blocked;
• user withdrawals remain enabled;
• liabilities can only stay flat or decrease.

Entry paths:

• authorized monitor / guardian;
• permissionless trigger once sequencer inactivity reaches the configured threshold.

Halted is the stronger containment state.

Financial transfers are frozen.

Entry paths:

• guardian action;
• permissionless insolvency trigger when:

assets < liabilities

Recovery requires all of:

delay elapsed
assets >= liabilities
sequencer age < inactivity threshold

A fresh heartbeat does not automatically restore Active mode.

This separation prevents a minimally active or compromised sequencer from clearing an incident state by itself.

The operational invariant suite verifies:

1. actual token assets always cover liabilities under modeled actions;
2. known user claims sum exactly to total liabilities;
3. all minted settlement assets remain accounted for;
4. once degraded, liabilities never increase;
5. once Halted, financial state is frozen;
6. mode cannot de-escalate in the harness because recovery is excluded from random incident actions.

The suite runs 256 invariant runs × 16,384 calls with zero handler reverts on the verified branch.

• monitor can stop new risk by entering ExitOnly;
• guardian can fully Halt;
• sequencer can update claims only while Active;
• owner controls delayed recovery;
• inactivity and insolvency trips are permissionless;
• production governance / key custody is outside this lab.

See INCIDENT_RUNBOOK.md for the response sequence and tooling.