# System Invariants

## Core Invariants

The DBIS system enforces strict invariants that **must** be maintained at all times. These invariants are checked on-chain and any violation causes transaction reversion.

## Position Invariants

### 1. Debt Never Increases
```
debtAfter <= debtBefore
```
After any amortization cycle, total debt value must never increase.

### 2. Collateral Never Decreases
```
collateralAfter >= collateralBefore
```
After any amortization cycle, total collateral value must never decrease.

### 3. Health Factor Never Worsens
```
healthFactorAfter >= healthFactorBefore
```
Health factor must always improve or stay the same.

### 4. LTV Never Worsens
```
LTV_after <= LTV_before
```
Loan-to-value ratio must never increase.

## Combined Invariant Check

All position invariants are checked together in `Vault.verifyPositionImproved()`:

```solidity
bool debtDecreased = debtAfter < debtBefore;
bool collateralIncreased = collateralAfter > collateralBefore;
bool hfImproved = healthFactorAfter > healthFactorBefore;

// All three must improve for strict amortization
return debtDecreased && collateralIncreased && hfImproved;
```

## Policy Invariants

### Flash Volume Limits
- Flash loan volume per asset per period ≤ configured limit
- Global flash loan volume per period ≤ configured limit

### Health Factor Thresholds
- Current HF ≥ minimum HF (from ConfigRegistry)
- HF improvement ≥ minimum improvement (for amortization)

### Provider Concentration
- No single provider can exceed maximum concentration percentage
- Diversification across providers enforced

### Liquidity Spreads
- Swap spreads ≤ maximum acceptable spread
- Liquidity depth ≥ minimum required depth

## Invariant Enforcement Points

1. **Pre-Execution**: GovernanceGuard verifies policy invariants
2. **During Execution**: Kernel enforces position changes
3. **Post-Execution**: Vault verifies position improvement
4. **On Revert**: All state changes rolled back

## Testing Invariants

### Unit Tests
- Test each invariant in isolation
- Test invariant violations cause reversion

### Integration Tests
- Test full cycles maintain invariants
- Test edge cases

### Fuzz Tests
- Random inputs verify invariants hold
- Stress test boundary conditions

### Invariant Tests (Foundry)
- Continuous invariant checking
- Property-based testing

## Failure Modes

### Invariant Violation Detection
When an invariant is violated:
1. Transaction reverts
2. Event emitted: `InvariantFail(reason)`
3. State unchanged (all changes rolled back)
4. MEV bot alerted

### Recovery Procedures
1. Analyze reason for failure
2. Adjust parameters if needed
3. Re-run with corrected parameters
4. Verify invariants before next cycle

## Formal Verification

Future work:
- Formal verification of invariant preservation
- Mathematical proofs of correctness
- Certified invariant checks