state-invariant-detection

# 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]
**I