# state-invariant-detection Detects broken mathematical relationships between state variables in smart contracts. Automatically infers invariants (totalSupply = sum(balances), conservation laws, ratio constraints) then finds functions that violate them. Catches unauthorized minting, broken tokenomics, accounting desynchronization, and state drift. Use when auditing for state-state invariant violations, broken accounting, supply mismatches, desynchronized state variables, or conservation law violations in smart contracts. - **Kind:** skill - **Source:** https://github.com/quillai-network/qs_skills - **Page:** https://forefy.com/skills/d34c3534-4ce1-4ec4-8f82-1bea653f4974 - **API (JSON + files):** https://forefy.com/api/asr/d34c3534-4ce1-4ec4-8f82-1bea653f4974 --- ## SKILL.md --- name: state-invariant-detection description: Detects broken mathematical relationships between state variables in smart contracts. Automatically infers invariants (totalSupply = sum(balances), conservation laws, ratio constraints) then finds functions that violate them. Catches unauthorized minting, broken tokenomics, accounting desynchronization, and state drift. Use when auditing for state-state invariant violations, broken accounting, supply mismatches, desynchronized state variables, or conservation law violations in smart contracts. --- # State Invariant Detection Automatically infer mathematical relationships between state variables, then find functions that **break those relationships**. Catches the most devastating DeFi vulnerabilities: unauthorized minting, broken tokenomics, accounting discrepancies, and state desynchronization. ## When to Use - Auditing token contracts for supply/balance mismatches - Analyzing staking, vault, or pool contracts for accounting errors - Detecting conservation law violations in treasury/fund management - Finding AMM/DEX constant product violations - Verifying that aggregate variables stay synchronized with individual records ## When NOT to Use - Guard-state consistency analysis (use semantic-guard-analysis) - Full multi-dimensional audit (use behavioral-state-analysis) - Entry point identification only (use entry-point-analyzer) ## Core Concept: State Variable Proportionality **Hypothesis:** In well-designed contracts, state variables maintain mathematical relationships (invariants) that should never be violated. When a function modifies one side of a relationship without updating the other, the invariant breaks — creating exploitable accounting errors. ## Five Types of State Relationships ### Type 1: Sum Relationships (Aggregation) ``` totalSupply = Σ balance[i] for all users i ``` **Found in:** ERC20 tokens, staking pools, vaults, share systems ### Type 2: Difference Relationships (Conservation) ``` totalFunds = availableFunds + lockedFunds ``` **Found in:** Treasuries, liquidity pools, vesting contracts ### Type 3: Ratio Relationships (Proportional) ``` k = reserveA × reserveB (constant product) sharePrice = totalAssets / totalShares ``` **Found in:** AMMs, DEXs, vault share pricing, collateralization ### Type 4: Monotonic Relationships (Ordering) ``` newValue ≥ oldValue (only increases) ``` **Found in:** Timestamps, nonces, accumulated rewards, total distributions ### Type 5: Synchronization Relationships (Coupling) ``` If stateA changes, stateB must change correspondingly ``` **Found in:** Deposit/mint pairs, burn/release pairs, collateral/borrowing power For detailed definitions and examples, see [{baseDir}/references/invariant-types.md]({baseDir}/references/invariant-types.md). ## The Three-Phase Detection Architecture ### Phase 1: State Variable Clustering Group state variables that appear to be related. **Algorithm:** ``` For each pair of state variables (A, B): 1. Track all functions that modify A 2. Track all functions that modify B 3. Calculate co-modification frequency: CoMod(A, B) = |Functions modifying both A and B| / |Functions modifying A or B| 4. If CoMod(A, B) > 0.6 → A and B are likely related ``` **Example:** ```solidity // mint() modifies BOTH totalSupply and balances → co-modified // burn() modifies BOTH totalSupply and balances → co-modified // transfer() modifies ONLY balances → does not co-modify CoMod(totalSupply, balances) = 2/3 = 66.7% Cluster identified: (totalSupply, balances) ``` ### Phase 2: Invariant Inference Determine the mathematical relationship between clustered variables. **Method 1 — Delta Pattern Matching:** ``` mint(): Δtotal = +amount, Δbalance = +amount → Same direction, same magnitude burn(): Δtotal = -amount, Δbalance = -amount → Same direction, same magnitude transfer(): Δbalance1 = -x, Δbalance2 = +x → Net zero change Inference: totalSupply = Σ balances (Aggregation invariant) ``` **Method 2 — Delta Correlation:** ``` If ΔA = ΔB in all cases → Direct proportional (A = B + constant) If ΔA = -ΔB in all cases → Inverse proportional (A + B = constant) If ΔA × constant = ΔB → Ratio relationship If ΔA occurs whenever ΔB → Synchronization invariant ``` **Method 3 — Expression Mining:** Parse actual code operations: ```solidity // Code: totalSupply += amount; balances[user] += amount; // Extracted: Δtotal = Δbalance // Inferred: total = Σ balances // Code: available = total - locked; // Extracted: available + locked = total // Inferred: Conservation law ``` **Invariant Confidence:** ``` Confidence(I) = |functions preserving I| / |functions modifying variables in I| ``` | Confidence | Classification | |-----------|---------------| | ≥ 90% | STRONG invariant | | 70-89% | MODERATE invariant | | < 70% | WEAK/NO invariant | ### Phase 3: Invariant Violation Detection Find functions that break established relationships. **Algorithm:** ``` For each inferred invariant I(stateA, stateB): For each function F that modifies stateA or stateB: Before: Capture (stateA, stateB) Simulate: Execute F After: Capture (stateA', stateB') If I(stateA, stateB) = True AND I(stateA', stateB') = False: → F is VULNERABLE ``` **Vulnerability Set:** ``` V_I = {F ∈ Functions | ∃σ : I(σ) = True ∧ I(F(σ)) = False} ``` ## Workflow ``` Task Progress: - [ ] Step 1: Identify all state variables in the contract - [ ] Step 2: Build co-modification matrix for all variable pairs - [ ] Step 3: Cluster related variables (CoMod > 0.6) - [ ] Step 4: Infer invariant type for each cluster (delta patterns) - [ ] Step 5: Test each function against inferred invariants - [ ] Step 6: Apply temporal filtering (only flag persistent violations) - [ ] Step 7: Score severity and generate report ``` ## Dual-Layer Integration This skill is **Layer 2** of the Semantic State Protocol. For maximum coverage, combine with **Layer 1** (semantic-guard-analysis): | Layer 1 Violation | Layer 2 Violation | Combined Severity | |-------------------|-------------------|-------------------| | Missing Guard | Breaks Invariant | **CRITICAL** | | Missing Guard | No Invariant Break | **HIGH** | | No Guard Issue | Breaks Invariant | **HIGH** | | No Guard Issue | No Invariant Break | **LOW/INFO** | ## Output Format ```markdown ## State-State Invariant Violation Report ### Finding: [Title] **Function:** `functionName()` at `Contract.sol:L42` **Severity:** [CRITICAL | HIGH | MEDIUM] **Invariant:** `[mathematical expression]` **Before Execution:** stateA = [value], stateB = [value] Invariant: [expression] = True ✓ **After Execution:** stateA = [value'], stateB = [value'] Invariant: [expression] = False ✗ **Root Cause:** [Which state variable was modified without updating its counterpart] **Impact:** [Accounting errors, inflated supply, broken pricing, exploitable drift] **Attack Scenario:** 1. [Step-by-step exploit leveraging the desynchronization] **Recommendation:** [Specific fix — add the missing state update] ``` ## Quick Detection Checklist When analyzing a contract, immediately check: - [ ] Does every function that modifies `balances` also update `totalSupply` (or have a valid reason not to)? - [ ] Does every function that moves between `available` and `locked` maintain `total = available + locked`? - [ ] Does every swap/trade function maintain the constant product `k = reserveA * reserveB`? - [ ] Do aggregate counters (`totalStaked`, `totalRewards`) stay synchronized with per-user mappings? - [ ] Are monotonic variables (nonces, timestamps) ever decremented? For detailed case studies, see [{baseDir}/references/case-studies.md]({baseDir}/references/case-studies.md). ## Rationalizations to Reject - "The totalSupply is just for display" → Protocols use totalSupply for share pricing, voting power, market cap — drift is exploitable - "Admin functions can bypass invariants" → Admin functions that break accounting create permanent protocol insolvency - "The difference is small" → Small accounting errors compound over time and transactions - "It's an emergency function" → Emergency functions that break state invariants create worse emergencies - "Transfer doesn't need to update totalSupply" → Correct, but verify the NET change in sum(balances) is zero ## references ``` ``` ## references/case-studies.md # State Invariant Detection Case Studies ## Case Study 1: The Broken Totalizer (ERC20 Token) ### Contract ```solidity contract BrokenToken { uint256 public totalSupply; mapping(address => uint256) public balances; function mint(address to, uint256 amount) public { totalSupply += amount; // ✓ Updates total balances[to] += amount; // ✓ Updates balance } function burn(address from, uint256 amount) public { totalSupply -= amount; // ✓ Updates total balances[from] -= amount; // ✓ Updates balance } function transfer(address to, uint256 amount) public { balances[msg.sender] -= amount; // ✓ Net-zero change balances[to] += amount; // ✓ in sum(balances) } function adminBurn(address from, uint256 amount) public onlyAdmin { // VULNERABILITY: Updates balance but NOT totalSupply balances[from] -= amount; } } ``` ### Detection **Phase 1 — Clustering:** ``` Functions modifying totalSupply: {mint, burn} Functions modifying balances: {mint, burn, transfer, adminBurn} CoMod(totalSupply, balances) = 2/4 = 50% ``` **Phase 2 — Invariant Inference:** ``` mint(): Δtotal = +amount, Δbalance = +amount → Same direction burn(): Δtotal = -amount, Δbalance = -amount → Same direction transfer(): Δtotal = 0, net Δbalance = 0 → Consistent Inferred: totalSupply = Σ balances Confidence: HIGH (holds in 3/3 analyzed functions) ``` **Phase 3 — Violation Detection:** ``` Testing adminBurn(): Before: totalSupply = 1000, Σbalances = 1000 → 1000 = 1000 ✓ Execute: adminBurn(alice, 100) After: totalSupply = 1000, Σbalances = 900 → 1000 ≠ 900 ✗ VULNERABILITY DETECTED! Severity: CRITICAL Invariant broken: totalSupply = Σ balances ``` **Impact:** - Protocol reports incorrect market cap - Share price calculations become wrong - Users can claim more value than exists - Accounting permanently desynchronized --- ## Case Study 2: The Desynced Staking Pool ### Contract ```solidity contract StakingPool { uint256 public totalStaked; uint256 public totalRewards; mapping(address => uint256) public userStake; mapping(address => uint256) public userRewards; function stake(uint256 amount) public { totalStaked += amount; userStake[msg.sender] += amount; } function unstake(uint256 amount) public { totalStaked -= amount; userStake[msg.sender] -= amount; } function distributeRewards() public { uint256 reward = calculateReward(msg.sender); userRewards[msg.sender] += reward; totalRewards += reward; } function emergencySlash(address user, uint256 penalty) public onlyAdmin { // VULN 1: Reduces user stake but not totalStaked userStake[user] -= penalty; } function compoundRewards() public { uint256 reward = userRewards[msg.sender]; userRewards[msg.sender] = 0; // Clears rewards userStake[msg.sender] += reward; // Adds to stake // VULN 2: Increases stake without updating totalStaked // VULN 3: Reduces rewards without updating totalRewards } } ``` ### Detection **Two invariants detected:** ``` Invariant 1: totalStaked = Σ userStake Invariant 2: totalRewards = Σ userRewards ``` **Three violations found:** ``` VULN 1: emergencySlash() breaks Invariant 1 Before: totalStaked=10000, Σstakes=10000 ✓ After: totalStaked=10000, Σstakes=9500 ✗ VULN 2: compoundRewards() breaks Invariant 1 Before: totalStaked=10000, Σstakes=10000 ✓ After: totalStaked=10000, Σstakes=10500 ✗ VULN 3: compoundRewards() breaks Invariant 2 Before: totalRewards=2000, Σrewards=2000 ✓ After: totalRewards=2000, Σrewards=1500 ✗ ``` --- ## Case Study 3: The Broken AMM Pool ### Contract ```solidity contract SimpleDEX { uint256 public reserveA; uint256 public reserveB; uint256 public kLast; function addLiquidity(uint256 amountA, uint256 amountB) public { reserveA += amountA; reserveB += amountB; kLast = reserveA * reserveB; // ✓ Updates k } function swap(uint256 amountAIn) public { uint256 amountBOut = getAmountOut(amountAIn); reserveA += amountAIn; reserveB -= amountBOut; kLast = reserveA * reserveB; // ✓ Updates k } function adminAdjustReserve(uint256 newReserveA) public onlyAdmin { // VULN: Changes reserve without updating k reserveA = newReserveA; } function emergencyDrain(uint256 amount) public onlyAdmin { // VULN: Removes liquidity without maintaining k reserveB -= amount; } } ``` ### Detection ``` Detected Relationship: Type: RATIO INVARIANT Pattern: kLast = reserveA × reserveB Confidence: 100% (2/2 normal functions maintain it) VULN 1: adminAdjustReserve() Before: reserveA=1000, reserveB=1000, k=1000000 After: reserveA=1500, reserveB=1000, k=1000000 (stale!) Expected k: 1500000 VULN 2: emergencyDrain() Before: reserveA=1000, reserveB=1000, k=1000000 After: reserveA=1000, reserveB=800, k=1000000 (stale!) Expected k: 800000 Impact: Constant product broken → price manipulation → arbitrage exploit ``` --- ## Case Study 4: The Conservation Law Violation ### Contract ```solidity contract Treasury { uint256 public totalFunds; uint256 public availableFunds; uint256 public lockedFunds; function deposit(uint256 amount) public { totalFunds += amount; availableFunds += amount; // ✓ total = available + locked maintained } function lockFunds(uint256 amount) public { availableFunds -= amount; lockedFunds += amount; // ✓ total unchanged, conservation holds } function emergencyUnlock(uint256 amount) public onlyAdmin { // VULN: Increases available without decreasing locked availableFunds += amount; } } ``` ### Detection ``` Conservation invariant: totalFunds = availableFunds + lockedFunds VULNERABILITY: emergencyUnlock() Before: total=1000, available=600, locked=400 1000 = 600 + 400 ✓ After: total=1000, available=700, locked=400 1000 ≠ 700 + 400 (1100) ✗ Impact: Funds created out of thin air! Available exceeds actual total. ``` --- ## Real-World Historical Examples ### The DAO Hack (2016) ``` Invariant violated: contract_balance = Σ user_balances Recursive call drained contract_balance without updating user_balances Result: $60M loss ``` ### Poly Network (2021) ``` Invariant violated: Cross-chain asset conservation Tokens burned on chain A ≠ tokens minted on chain B Result: $600M loss ``` ### Indexed Finance (2021) ``` Invariant violated: Pool weight proportionality Spot price used instead of TWAP for weight calculations Result: $16M loss ``` ### Audius (2022) ``` Invariant violated: Governance token supply conservation Malicious proposal minted tokens without corresponding delegated votes Result: $6M loss ``` ## references/invariant-types.md # State-State Invariant Types — Detailed Reference ## Type 1: Sum Relationships (Aggregation Invariants) **Formula:** ``` s_total = Σᵢ sᵢ ``` **Pattern:** An aggregate variable equals the sum of all individual entries. **Real-World Examples:** | Protocol Type | Aggregate | Individual | Invariant | |--------------|-----------|------------|-----------| | ERC20 Token | `totalSupply` | `balances[user]` | `totalSupply = Σ balances` | | Staking Pool | `totalStaked` | `userStake[user]` | `totalStaked = Σ userStakes` | | Vault | `totalAssets` | `userDeposits[user]` | `totalAssets = Σ deposits` | | Share System | `totalShares` | `shares[user]` | `totalShares = Σ shares` | | Reward Pool | `totalRewards` | `userRewards[user]` | `totalRewards = Σ userRewards` | **Valid Exception:** `transfer()` modifies individual balances without changing totalSupply — this is correct because the net change in sum(balances) is zero. **Detection Signal:** If a function adds to a user's balance without incrementing the total (or vice versa), the invariant is broken. --- ## Type 2: Difference Relationships (Conservation Invariants) **Formula:** ``` Σᵢ sᵢ = constant (within a transaction or epoch) ``` **Pattern:** Value is neither created nor destroyed, just moved between categories. **Real-World Examples:** | Protocol Type | Conservation Law | |--------------|-----------------| | Treasury | `totalFunds = available + locked` | | Liquidity Pool | `totalLiquidity = active + reserved` | | Vesting | `totalAllocated = vested + unvested` | | Escrow | `totalDeposited = released + held` | | Loan | `totalCollateral = free + pledged` | **Detection Signal:** If a function increases one category without decreasing another (or without changing the total), conservation is violated. --- ## Type 3: Ratio Relationships (Proportional Invariants) **Formula:** ``` s₁ / s₂ = k (constant under specific operations) ``` Or product form: ``` s₁ × s₂ = k (constant product) ``` **Real-World Examples:** | Protocol Type | Ratio Invariant | |--------------|----------------| | AMM (Uniswap) | `k = reserveToken0 × reserveToken1` | | Vault Shares | `sharePrice = totalAssets / totalShares` | | Collateralized Debt | `collateralRatio = collateral / debt > 1.5` | | Rebasing Token | `internalBalance = externalBalance × rebaseFactor` | **Detection Signal:** If a function modifies one reserve without updating `k`, or changes assets without proportionally adjusting shares. **Note:** The constant product `k` can legitimately change during `addLiquidity` and `removeLiquidity` — only swaps should preserve it. --- ## Type 4: Monotonic Relationships (Ordering Invariants) **Formula:** ``` s_new ≥ s_old for all state transitions (monotonically increasing) s_new ≤ s_old for all state transitions (monotonically decreasing) ``` **Real-World Examples:** | Variable | Direction | Invariant | |----------|-----------|-----------| | `nonce` | Increasing | Never reused, always increments | | `lastUpdateTime` | Increasing | Time only moves forward | | `totalRewardsDistributed` | Increasing | Distributed rewards never decrease | | `totalBurned` | Increasing | Cumulative burn count | | `remainingAllocation` | Decreasing | Allocation depletes over time | **Detection Signal:** If any function decrements a monotonically increasing variable, the invariant is broken. --- ## Type 5: Synchronization Relationships (Coupling Invariants) **Formula:** ``` If Δs₁ ≠ 0, then Δs₂ must be f(Δs₁) ``` Where `f` is a deterministic function of the change. **Real-World Examples:** | Trigger Change | Required Corresponding Change | |----------------|------------------------------| | User balance increases | totalSupply increases by same amount | | Collateral deposited | Borrowing power increases proportionally | | Shares burned | Underlying assets released | | Stake added | Reward rate recalculated | | Liquidity added | LP tokens minted proportionally | | Oracle price updated | Liquidation thresholds recalculated | **Detection Signal:** If a function modifies the trigger variable without touching the coupled variable, the synchronization is broken. --- ## Invariant Inference Methods ### Method 1: Code Pattern Matching Analyze how variables change together across functions: ``` mint(): totalSupply += x, balance += x → Same direction, same magnitude burn(): totalSupply -= x, balance -= x → Same direction, same magnitude transfer(): balance1 -= x, balance2 += x → Zero-sum within balances ``` ### Method 2: Delta Correlation ```python For variables A and B that change together: deltas = [] for each function F: delta_A = change_in(A) delta_B = change_in(B) if delta_B != 0: ratio = delta_A / delta_B deltas.append(ratio) if std_deviation(deltas) < threshold: coefficient = mean(deltas) invariant = f"A = {coefficient} × B" ``` ### Method 3: Expression Mining Parse code expressions to extract relationships: ```solidity // Code: available = total - locked // Extracted: available + locked = total // Type: Conservation // Code: shares = assets * PRECISION / sharePrice // Extracted: shares * sharePrice = assets * PRECISION // Type: Ratio ``` ### Method 4: State Snapshot Analysis ``` Before function: [totalSupply = 1000, sum(balances) = 1000] After function: [totalSupply = 1100, sum(balances) = 1100] Consistency: totalSupply == sum(balances) ✓ After 10+ functions: If holds 100%: STRONG invariant If holds 70-99%: MODERATE invariant If holds <70%: WEAK/NO invariant ``` --- ## Cross-Function State Flow Track state changes through internal call chains: ``` depositAssets() → mintShares() → [totalShares, userShares] Transitive modifications: - depositAssets directly modifies: totalAssets - depositAssets indirectly modifies: totalShares, userShares Invariant: If totalAssets changes, totalShares should also change This holds even through indirect calls. ``` --- ## Temporal Invariant Handling Some invariants temporarily break during execution: ```solidity function bid() public payable { highestBid = msg.value; // Temporarily breaks invariant require(msg.value > highestBid); // Validates (reverts if broken) highestBidder = msg.sender; // Restores invariant } ``` **Rule:** Only flag violations that **persist at function exit** (successful completion). Reverts restore the invariant.