prediction markets

.gitignore

@@ -9,4 +9,10 @@ out/
 # Dotenv file
 .env
 
-/node_modules
+/node_modules
+
+# macOS Finder metadata
+.DS_Store
+
+# Local gas snapshot generated by prediction market integration tests
+snapshots/PredictionMarketIntegration.json

docs/PredictionMarketIntegrationGuide.md

@@ -0,0 +1,151 @@
+# Prediction Market Integration Guide
+
+This guide describes how to integrate prediction markets with `Airlock` using `PredictionMigrator`.
+
+## Overview
+
+The prediction market flow has 3 stages:
+
+1. `create`: register each market entry (`token`) with `(oracle, entryId)` in `PredictionMigrator`.
+2. `migrate`: move proceeds into the market pot after oracle finalization.
+3. `claim`: winning token holders claim pro-rata numeraire.
+
+Reference implementation:
+- `src/migrators/PredictionMigrator.sol`
+- `test/integration/PredictionMarket.t.sol`
+
+## Required Components
+
+- `Airlock`
+- `PredictionMigrator` as a whitelisted `LiquidityMigrator` module
+- Token factory that creates burnable entry tokens (`burn(uint256)` required)
+- Pool initializer (`DopplerHookInitializer` in current integration)
+- Prediction oracle implementing `IPredictionOracle`
+- Optional governance factory (`NoOpGovernanceFactory` is commonly used)
+
+## Critical Integration Requirements
+
+- Entry tokens must support `burn(uint256)`.
+  - If burn is unavailable/restricted, `migrate` reverts.
+- A market is keyed by `oracle` and has exactly one numeraire.
+  - First entry sets numeraire; later entries for same oracle must match.
+- `migrate` expects exactly one registered entry token in `(token0, token1)`.
+  - Both registered or neither registered reverts.
+- Oracle must be finalized before migration and before first successful claim.
+
+## Step-By-Step Integration
+
+### 1) Deploy and Whitelist Modules
+
+Deploy `PredictionMigrator(airlock)` and whitelist it with:
+
+```solidity
+address[] memory modules = new address[](1);
+modules[0] = address(predictionMigrator);
+ModuleState[] memory states = new ModuleState[](1);
+states[0] = ModuleState.LiquidityMigrator;
+airlock.setModuleState(modules, states);
+```
+
+For the hook-based flow, deploy and register `NoSellDopplerHook` on `DopplerHookInitializer`.
+
+### 2) Create Each Entry
+
+For each market entry token, call `airlock.create` with:
+
+- `liquidityMigrator = predictionMigrator`
+- `liquidityMigratorData = abi.encode(oracle, entryId)`
+- shared market numeraire for all entries under the same `oracle`
+
+Example:
+
+```solidity
+CreateParams memory params = CreateParams({
+    initialSupply: 1_000_000 ether,
+    numTokensToSell: 1_000_000 ether,
+    numeraire: numeraire,
+    tokenFactory: tokenFactory,
+    tokenFactoryData: tokenFactoryData,
+    governanceFactory: governanceFactory,
+    governanceFactoryData: governanceFactoryData,
+    poolInitializer: dopplerInitializer,
+    poolInitializerData: poolInitializerData,
+    liquidityMigrator: predictionMigrator,
+    liquidityMigratorData: abi.encode(address(oracle), entryId),
+    integrator: address(0),
+    salt: salt
+});
+```
+
+During `create`, `PredictionMigrator.initialize` stores:
+- token -> oracle mapping
+- `(oracle, token) -> entryId`
+- entry state (unmigrated)
+
+### 3) Finalize the Oracle
+
+Before migration, oracle must return `(winner, isFinalized=true)` from:
+
+```solidity
+getWinner(address oracle) returns (address winningToken, bool isFinalized)
+```
+
+### 4) Migrate Each Entry
+
+Call `airlock.migrate(entryToken)` per entry after graduation/finalization conditions are met.
+
+`PredictionMigrator.migrate`:
+- validates pair has exactly one registered entry token
+- checks oracle finalization
+- checks pair numeraire matches market numeraire
+- computes proceeds delta using global per-numeraire accounting
+- computes `claimableSupply = totalSupply - unsoldBalance`
+- burns unsold entry tokens
+- updates entry contribution and market pot
+
+### 5) Claim Winnings
+
+Users claim with winning tokens:
+
+1. approve winning token to `PredictionMigrator`
+2. optionally `previewClaim(oracle, tokenAmount)`
+3. call `claim(oracle, tokenAmount)`
+
+Payout math:
+
+```text
+claimAmount = mulDiv(tokenAmount, market.totalPot, winningEntry.claimableSupply)
+```
+
+## Shared-Numeraire Accounting Model
+
+`PredictionMigrator` tracks a global per-numeraire accounted balance:
+
+- migration contribution = `currentBalance(numeraire) - accounted[numeraire]`
+- after migration: `accounted[numeraire] = currentBalance`
+- on claim payout: `accounted[numeraire] -= claimAmount`
+
+This prevents cross-market contamination when multiple markets share the same numeraire.
+
+## Common Reverts and Meaning
+
+- `EntryNotRegistered`: token pair does not include a registered entry
+- `InvalidTokenPair`: both tokens (or ambiguous pair) are registered entries
+- `NumeraireMismatch`: entry migrated with wrong quote token
+- `OracleNotFinalized`: oracle is not finalized yet
+- `AlreadyMigrated`: entry already migrated
+- `WinningEntryNotMigrated`: claim attempted before winning entry migration
+- `AccountingInvariant`: unexpected external balance drift vs accounted state
+
+## Test Checklist
+
+Run these before production:
+
+```bash
+forge test --match-path test/unit/migrators/PredictionMigrator.t.sol
+forge test --match-path test/integration/PredictionMarket.t.sol
+forge test --match-path test/invariant/PredictionMigrator/PredictionMigratorInvariants.t.sol
+forge test --match-path test/invariant/PredictionMigrator/PredictionMigratorEthInvariants.t.sol
+FOUNDRY_PROFILE=deep forge test --match-path test/invariant/PredictionMigrator/PredictionMigratorInvariants.t.sol
+FOUNDRY_PROFILE=deep forge test --match-path test/invariant/PredictionMigrator/PredictionMigratorEthInvariants.t.sol
+```

specs/SPEC-prediction-markets-high-level-v1.0.1.md

@@ -0,0 +1,152 @@
+# Doppler Prediction Markets High-Level Spec (v1.0.1)
+
+## 1. Purpose
+
+Define the high-level behavior and integration requirements for prediction markets built on Doppler + Airlock using `PredictionMigrator`.
+
+This spec captures the production posture after:
+
+- global per-numeraire accounting hardening
+- strict burnable-asset migration requirement
+- invariant harness expansion (ERC20 and ETH numeraires)
+
+## 2. Scope
+
+In scope:
+
+- market entry registration at `create`
+- proceeds migration at `migrate`
+- winner claims
+- multi-market shared-numeraire correctness
+
+Out of scope:
+
+- oracle design details beyond `IPredictionOracle` surface
+- front-end UX implementation details
+- non-Doppler auction mechanics
+
+## 3. Architecture
+
+Core contracts:
+
+- `Airlock` orchestrates create/migrate lifecycle and module dispatch
+- `PredictionMigrator` tracks entries, pots, claims, and payout accounting
+- `IPredictionOracle` reports winner + finalization state
+- Doppler hook stack (including `NoSellDopplerHook`) constrains market behavior
+
+Market identity:
+
+- A market is keyed by `oracle` address.
+- Each market contains one or more entries (`entryId`, token pairs).
+- All entries in a market must share a single numeraire.
+
+## 4. Lifecycle
+
+### 4.1 Create / Initialize
+
+For each entry creation:
+
+1. Airlock calls `PredictionMigrator.initialize(asset, numeraire, abi.encode(oracle, entryId))`.
+2. Migrator enforces uniqueness:
+   - `(oracle, asset)` must not already map to an entry
+   - `(oracle, entryId)` must be unused
+3. First entry sets market numeraire; later entries must match.
+4. Entry is registered but not migrated.
+
+### 4.2 Migrate
+
+When Airlock migrates an entry:
+
+1. Pair validation: exactly one token in `(token0, token1)` must be a registered entry token.
+2. Oracle must be finalized.
+3. Pair numeraire must match market numeraire.
+4. Contribution is inferred via global per-numeraire balance delta:
+   - `delta = currentBalance(numeraire) - accounted[numeraire]`
+   - `accounted[numeraire] = currentBalance(numeraire)`
+5. Unsold entry tokens are removed via strict `burn(assetBalance)`.
+6. Entry and market accounting updates:
+   - `entry.contribution += delta` (single migration per entry in current model)
+   - `entry.claimableSupply = totalSupply - unsold`
+   - `entry.isMigrated = true`
+   - `market.totalPot += delta`
+
+### 4.3 Claim
+
+For winning token holders:
+
+1. Market resolves lazily on first claim if not cached:
+   - fetch winner from oracle
+   - require finalized
+2. Winning entry must already be migrated.
+3. Claim payout:
+   - `claimAmount = mulDiv(tokenAmount, market.totalPot, winningEntry.claimableSupply)`
+4. Winning tokens are transferred from claimer to migrator.
+5. Accounting updates before payout transfer:
+   - `market.totalClaimed += claimAmount`
+   - `accounted[numeraire] -= claimAmount`
+6. Numeraire is transferred to claimer.
+
+## 5. Security and Correctness Properties
+
+1. Shared-numeraire isolation:
+   - migrations in market A do not contaminate market B contributions.
+2. Claim/migrate interleaving safety:
+   - claims between migrations preserve correct later migration deltas.
+3. Pair-shape safety:
+   - both-registered and neither-registered pair shapes revert.
+4. Numeraire consistency:
+   - market-level numeraire cannot drift across entries.
+5. Burnability enforcement:
+   - non-burnable entry tokens are unsupported and migration reverts.
+6. Reentrancy hardening:
+   - `claim` is protected by `ReentrancyGuard`.
+
+## 6. Integration Requirements
+
+Required:
+
+- whitelist `PredictionMigrator` as a `LiquidityMigrator` module in Airlock
+- use burnable entry tokens implementing `burn(uint256)`
+- ensure all entries under one oracle use same numeraire
+- ensure oracle finalization semantics are trustworthy
+
+Recommended:
+
+- keep sell paths disabled with `NoSellDopplerHook` where applicable
+- surface claim timing UX warning:
+  - claiming before all entries migrate can produce lower payout than waiting
+
+## 7. Error Surface (High Level)
+
+- `EntryAlreadyExists`
+- `EntryIdAlreadyUsed`
+- `EntryNotRegistered`
+- `InvalidTokenPair`
+- `NumeraireMismatch`
+- `OracleNotFinalized`
+- `AlreadyMigrated`
+- `WinningEntryNotMigrated`
+- `AccountingInvariant`
+
+## 8. Verification Strategy
+
+Production gating test stack:
+
+- unit: `test/unit/migrators/PredictionMigrator.t.sol`
+- integration: `test/integration/PredictionMarket.t.sol`
+- invariants (ERC20): `test/invariant/PredictionMigrator/PredictionMigratorInvariants.t.sol`
+- invariants (ETH): `test/invariant/PredictionMigrator/PredictionMigratorEthInvariants.t.sol`
+- deep invariant profile (`FOUNDRY_PROFILE=deep`) for both invariant suites
+
+Invariant themes:
+
+- on-chain market/entry state matches ghost state
+- global migrator numeraire balance equals net contributed minus claimed
+- global ghost sums equal sum of per-market ghosts
+
+## 9. References
+
+- Implementation: `src/migrators/PredictionMigrator.sol`
+- Interface: `src/interfaces/IPredictionMigrator.sol`
+- Integration guide: `docs/PredictionMarketIntegrationGuide.md`
+- Invariant harness spec: `specs/prediction-migrator-invariant-harness-spec.md`