Example: AMM/DEX contract with constant-product proofs

[Th0rgal]

Why

The constant-product AMM (x*y=k) is the #1 DeFi primitive (Uniswap V2 model). Verity currently has no example demonstrating non-trivial mathematical invariant proofs. An AMM example would:

• Prove the system handles real DeFi math (multiplication, division, overflow reasoning)
• Demonstrate invariant preservation across swap/addLiquidity/removeLiquidity
• Serve as a reference for users building DEX contracts
• Stress-test the proof automation with arithmetic-heavy properties

Scope

Minimal AMM contract with:

• addLiquidity(amount0, amount1) — deposit token pair
• removeLiquidity(shares) — withdraw proportionally
• swap(tokenIn, amountIn) — constant-product swap with fee

Key properties to prove:

• Invariant preservation: reserve0 * reserve1 >= k after every swap (with fee)
• No value extraction: swapping back and forth cannot increase holdings
• Liquidity share accounting: shares correctly represent proportional ownership
• Overflow safety: all arithmetic stays within Uint256 bounds under stated preconditions

Prerequisites

• May need additional Uint256 multiplication/division lemmas in Stdlib/Math.lean
• mulDivDown/mulDivUp already exist in the EDSL — proofs for these would be needed

Effort

3-4 weeks

Acceptance

• AMM contract defined in EDSL (or verity_contract)
• Formal specs for all 3 operations
• Constant-product invariant proven with zero sorry
• Differential tests passing

[Th0rgal]

Deferring — the project needs architectural simplification before adding new contract surface area. Current priorities:

1. Unify to macro-only contract authoring path
2. Remove hardcoded counts from docs
3. Finish CompilationModel.lean split
4. Trim CI script sprawl
5. Complete package decoupling

Will revisit once the architecture is cleaner and contribution barrier is lower.