Skip to content

Commit 0937846

Browse files
committed
feat: add Types.sol and GaussianMath.sol
Core types, constants, and Gaussian math library with full Normal PDF normalization, geometric side check in verifyMinPoint, and L₂ self-norm in computeFormulaMin.
1 parent c538f16 commit 0937846

2 files changed

Lines changed: 264 additions & 0 deletions

File tree

src/libraries/GaussianMath.sol

Lines changed: 144 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,144 @@
1+
// SPDX-License-Identifier: MIT
2+
pragma solidity ^0.8.24;
3+
4+
import {SD59x18, convert, ZERO} from "@prb/math/SD59x18.sol";
5+
import {SQRT_PI, SQRT_TWO_PI, EPSILON, DUST_THRESHOLD, NORM_TOLERANCE} from "../types/Types.sol";
6+
import {InvalidNorm, NotCriticalPoint, NotMinimum, WrongSide, DustPosition} from "../types/Types.sol";
7+
8+
/// @title GaussianMath
9+
/// @notice Pure math library for Gaussian PDF evaluation and verification.
10+
/// @dev All functions use PRBMath SD59x18 fixed-point arithmetic.
11+
/// The Gaussian is f(x) = λ/(σ·√(2π)) · exp(−(x−μ)²/(2σ²))
12+
/// i.e. f = λ · φ(x; μ, σ) where φ is the standard Normal PDF.
13+
library GaussianMath {
14+
/// @notice Evaluate f(x) = λ/(σ·√(2π)) · exp(−(x−μ)²/(2σ²))
15+
function eval(SD59x18 mu, SD59x18 lambda, SD59x18 sigma, SD59x18 x) internal pure returns (SD59x18) {
16+
SD59x18 amplitude = lambda / (sigma * SQRT_TWO_PI);
17+
return amplitude * _expTerm(mu, sigma, x);
18+
}
19+
20+
/// @notice First derivative: f'(x) = −(x−μ)/σ² · f(x)
21+
function derivative(SD59x18 mu, SD59x18 lambda, SD59x18 sigma, SD59x18 x) internal pure returns (SD59x18) {
22+
SD59x18 diff = mu - x;
23+
SD59x18 sigmaSq = sigma * sigma;
24+
return (diff / sigmaSq) * eval(mu, lambda, sigma, x);
25+
}
26+
27+
/// @notice Second derivative: f''(x) = ((x−μ)²/σ⁴ − 1/σ²) · f(x)
28+
function secondDerivative(SD59x18 mu, SD59x18 lambda, SD59x18 sigma, SD59x18 x)
29+
internal
30+
pure
31+
returns (SD59x18)
32+
{
33+
SD59x18 diff = x - mu;
34+
SD59x18 sigmaSq = sigma * sigma;
35+
SD59x18 factor = (diff * diff) / (sigmaSq * sigmaSq) - convert(1) / sigmaSq;
36+
return factor * eval(mu, lambda, sigma, x);
37+
}
38+
39+
/// @notice Verify the L₂ norm invariant: λ² ≈ 2·k²·σ·√π
40+
/// @dev Uses relative tolerance NORM_TOLERANCE (0.1%).
41+
function verifyNorm(SD59x18 lambda, SD59x18 sigma, SD59x18 kSquared) internal pure {
42+
SD59x18 lhs = lambda * lambda;
43+
SD59x18 rhs = convert(2) * kSquared * sigma * SQRT_PI;
44+
45+
SD59x18 diff = lhs > rhs ? lhs - rhs : rhs - lhs;
46+
SD59x18 maxVal = lhs > rhs ? lhs : rhs;
47+
48+
if (diff / maxVal > NORM_TOLERANCE) revert InvalidNorm();
49+
}
50+
51+
/// @notice 4-check min-point verification for collateral calculation.
52+
/// @param fMu Current aggregate mean
53+
/// @param fLambda Current aggregate lambda
54+
/// @param fSigma Current aggregate sigma
55+
/// @param gMu Proposed new aggregate mean
56+
/// @param gLambda Proposed new aggregate lambda
57+
/// @param gSigma Proposed new aggregate sigma
58+
/// @param candidate The x-coordinate of the claimed minimum of g(x)−f(x)
59+
/// @return minValue The (negative) value g(candidate)−f(candidate); collateral = −minValue
60+
function verifyMinPoint(
61+
SD59x18 fMu,
62+
SD59x18 fLambda,
63+
SD59x18 fSigma,
64+
SD59x18 gMu,
65+
SD59x18 gLambda,
66+
SD59x18 gSigma,
67+
SD59x18 candidate
68+
) internal pure returns (SD59x18 minValue) {
69+
// Check 1: Critical point — |g'(x) − f'(x)| < EPSILON
70+
SD59x18 gPrime = derivative(gMu, gLambda, gSigma, candidate);
71+
SD59x18 fPrime = derivative(fMu, fLambda, fSigma, candidate);
72+
SD59x18 firstDerivDiff = gPrime - fPrime;
73+
if (firstDerivDiff < ZERO) firstDerivDiff = -firstDerivDiff;
74+
if (firstDerivDiff > EPSILON) revert NotCriticalPoint();
75+
76+
// Check 2: Minimum — g''(x) − f''(x) > 0
77+
SD59x18 gDoublePrime = secondDerivative(gMu, gLambda, gSigma, candidate);
78+
SD59x18 fDoublePrime = secondDerivative(fMu, fLambda, fSigma, candidate);
79+
if (gDoublePrime - fDoublePrime < ZERO) revert NotMinimum();
80+
81+
// Check 3: Geometric side check — candidate must be on opposite side of g's mean from f's mean
82+
if (gMu > fMu) {
83+
if (candidate >= fMu) revert WrongSide();
84+
} else if (gMu < fMu) {
85+
if (candidate <= fMu) revert WrongSide();
86+
} else {
87+
// Equal means: minimum is in the tails, candidate must be at least 1σ from shared mean
88+
SD59x18 dist = candidate - fMu;
89+
if (dist < ZERO) dist = -dist;
90+
if (dist < fSigma) revert WrongSide();
91+
}
92+
93+
// Value computation (for Check 4 and return value)
94+
SD59x18 gVal = eval(gMu, gLambda, gSigma, candidate);
95+
SD59x18 fVal = eval(fMu, fLambda, fSigma, candidate);
96+
minValue = gVal - fVal;
97+
98+
// Check 4: Dust threshold — min value is meaningfully negative
99+
if (minValue > -DUST_THRESHOLD) revert DustPosition();
100+
}
101+
102+
/// @notice Derive lambda from the invariant: λ = √(2·k²·σ·√π)
103+
function computeLambda(SD59x18 kSquared, SD59x18 sigma) internal pure returns (SD59x18) {
104+
SD59x18 inner = convert(2) * kSquared * sigma * SQRT_PI;
105+
return inner.sqrt();
106+
}
107+
108+
/// @notice Closed-form min of g(x)−f(x) for cross-checking in tests.
109+
/// @dev m = λ_g/(2·σ_g·√π) − λ_f/√(2π·(σ_f²+σ_g²)) · exp(−(μ_f−μ_g)²/(2·(σ_f²+σ_g²)))
110+
function computeFormulaMin(
111+
SD59x18 fMu,
112+
SD59x18 fLambda,
113+
SD59x18 fSigma,
114+
SD59x18 gMu,
115+
SD59x18 gLambda,
116+
SD59x18 gSigma
117+
) internal pure returns (SD59x18) {
118+
// Term 1: Self-norm — λ_g / (2·σ_g·√π)
119+
SD59x18 selfNorm = gLambda / (convert(2) * gSigma * SQRT_PI);
120+
121+
// Combined sigma for the cross-term
122+
SD59x18 fSigmaSq = fSigma * fSigma;
123+
SD59x18 gSigmaSq = gSigma * gSigma;
124+
SD59x18 combinedSigmaSq = fSigmaSq + gSigmaSq;
125+
SD59x18 combinedSigma = combinedSigmaSq.sqrt();
126+
127+
// Cross-term amplitude: λ_f / (√(2π) · combinedSigma)
128+
SD59x18 crossAmplitude = fLambda / (SQRT_TWO_PI * combinedSigma);
129+
130+
// Cross-term exponent: −(μ_f − μ_g)² / (2·(σ_f² + σ_g²))
131+
SD59x18 muDiff = fMu - gMu;
132+
SD59x18 exponent = -(muDiff * muDiff) / (convert(2) * combinedSigmaSq);
133+
SD59x18 crossTerm = crossAmplitude * exponent.exp();
134+
135+
return selfNorm - crossTerm;
136+
}
137+
138+
/// @dev Shared exponential term: exp(−(x−μ)²/(2σ²))
139+
function _expTerm(SD59x18 mu, SD59x18 sigma, SD59x18 x) private pure returns (SD59x18) {
140+
SD59x18 diff = x - mu;
141+
SD59x18 exponent = -(diff * diff) / (convert(2) * sigma * sigma);
142+
return exponent.exp();
143+
}
144+
}

src/types/Types.sol

Lines changed: 120 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,120 @@
1+
// SPDX-License-Identifier: MIT
2+
pragma solidity ^0.8.24;
3+
4+
import {SD59x18} from "@prb/math/SD59x18.sol";
5+
6+
// ═══════════════════════════════════════════════════════════════════════
7+
// ENUMS
8+
// ═══════════════════════════════════════════════════════════════════════
9+
10+
enum MarketSize {
11+
SMALL,
12+
MEDIUM,
13+
LARGE
14+
}
15+
16+
// ═══════════════════════════════════════════════════════════════════════
17+
// STRUCTS
18+
// ═══════════════════════════════════════════════════════════════════════
19+
20+
/// @notice Snapshot of a trader's prediction position (before and after Gaussian state).
21+
struct Position {
22+
int128 f_mu;
23+
int128 f_lambda;
24+
uint128 f_sigma;
25+
int128 g_mu;
26+
int128 g_lambda;
27+
uint128 g_sigma;
28+
uint128 collateral;
29+
address trader;
30+
uint64 marketId;
31+
bool settled;
32+
}
33+
34+
/// @notice Full state of a prediction market.
35+
struct Market {
36+
// Current aggregate Gaussian state
37+
int128 mu;
38+
int128 lambda;
39+
uint128 sigma;
40+
// CFMM invariant (derived from MarketSize)
41+
uint128 k_squared;
42+
// Minimum allowed sigma (derived as initSigma / 10)
43+
uint128 minSigma;
44+
// Initial state (for zero-sum verification)
45+
int128 initialMu;
46+
int128 initialLambda;
47+
uint128 initialSigma;
48+
// Oracle
49+
address chainlinkFeed;
50+
uint64 resolutionTime;
51+
int128 resolvedOutcome;
52+
bool resolved;
53+
// Accounting
54+
uint128 totalCollateralHeld;
55+
}
56+
57+
// ═══════════════════════════════════════════════════════════════════════
58+
// CONSTANTS
59+
// ═══════════════════════════════════════════════════════════════════════
60+
61+
/// @dev √π in SD59x18 (18 decimals)
62+
SD59x18 constant SQRT_PI = SD59x18.wrap(1_772453850905516027);
63+
64+
/// @dev √(2π) in SD59x18
65+
SD59x18 constant SQRT_TWO_PI = SD59x18.wrap(2_506628274631000502);
66+
67+
/// @dev Operation type byte for prediction trades
68+
uint8 constant OP_TRADE = 1;
69+
70+
/// @dev 0.3% open fee (30 basis points)
71+
uint256 constant OPEN_FEE_BPS = 30;
72+
73+
/// @dev 2.5% profit fee (250 basis points)
74+
uint256 constant PROFIT_FEE_BPS = 250;
75+
76+
/// @dev Fee denominator (10_000 = 100%)
77+
uint256 constant FEE_DENOMINATOR = 10_000;
78+
79+
/// @dev Tolerance for first-derivative zero check in min-point verification.
80+
/// 1e14 ≈ 1e-4 in real terms — accounts for fixed-point rounding.
81+
SD59x18 constant EPSILON = SD59x18.wrap(1e14);
82+
83+
/// @dev Minimum meaningful position value. Positions with |minValue| below this are rejected.
84+
/// 1e12 ≈ 1e-6 in real terms.
85+
SD59x18 constant DUST_THRESHOLD = SD59x18.wrap(1e12);
86+
87+
/// @dev Maximum staleness for Chainlink oracle answers (1 hour)
88+
uint256 constant MAX_STALENESS = 1 hours;
89+
90+
/// @dev Relative tolerance for norm verification (0.1% = 1e15 out of 1e18)
91+
SD59x18 constant NORM_TOLERANCE = SD59x18.wrap(1e15);
92+
93+
/// @dev MarketSize presets for k_squared (SD59x18 scale)
94+
uint128 constant K_SQUARED_SMALL = 1_000e18;
95+
uint128 constant K_SQUARED_MEDIUM = 10_000e18;
96+
uint128 constant K_SQUARED_LARGE = 100_000e18;
97+
98+
// ═══════════════════════════════════════════════════════════════════════
99+
// ERRORS
100+
// ═══════════════════════════════════════════════════════════════════════
101+
102+
error InvalidNorm();
103+
error SigmaTooLow();
104+
error NotCriticalPoint();
105+
error NotMinimum();
106+
error WrongSide();
107+
error DustPosition();
108+
error MarketNotResolved();
109+
error MarketAlreadyResolved();
110+
error ResolutionTooEarly();
111+
error StaleOracle();
112+
error InvalidOracle();
113+
error NotPositionOwner();
114+
error AlreadySettled();
115+
error UnknownOperation();
116+
error MarketResolved();
117+
error InvalidSigma();
118+
error InvalidFeed();
119+
error ResolutionInPast();
120+
error PoolAlreadyRegistered();

0 commit comments

Comments
 (0)