Math: create verity-math package with verified exp, ln, pow, WAD/RAY helpers

[Th0rgal]

Summary

Create a separate Lean package (verity-math) providing a verified fixed-point math library built on top of the Phase 1 compiler built-ins (#1622). This is the Verity equivalent of PRBMath / Solmate FixedPointMathLib — but with machine-checked correctness proofs and proven error bounds.

This is deferred until #1622 (Phase 1 built-ins) and #1623 (loop semantics fix) are complete.

Motivation

In Solidity, math libraries like PRBMath provide exp, ln, pow, sqrt — but correctness is only validated by fuzzing. Verity can prove these implementations correct against Lean/Mathlib's real analysis, with proven error bounds (e.g., "result is within 1 ULP of the true value"). This is a genuine differentiator.

Package structure

verity-math/                    # Separate Lean package, imports verity
  lakefile.lean                 # depends on verity (EDSL + compiler)
  VerityMath/
    FixedPoint/
      WAD.lean                  # UD60x18-equivalent (18 decimals)
      RAY.lean                  # 27-decimal precision
      Conversions.lean          # wadToRay, rayToWad, etc.
    Functions/
      Exp.lean                  # exp(x) = e^x, WAD-scaled
      Ln.lean                   # ln(x), WAD-scaled
      Pow.lean                  # pow(base, exp), WAD-scaled
      ExpWad.lean               # combined exp/ln for WAD
      Compound.lean             # continuous compounding helpers
    Proofs/
      Exp/Correctness.lean      # exp matches Mathlib Real.exp within error bound
      Exp/ErrorBound.lean       # |result - true_value| ≤ 1 ULP
      Ln/Correctness.lean
      Pow/Correctness.lean
      Conversions/Lossless.lean # wadToRay is exact (no precision loss)
    Specs/
      FixedPointSpec.lean       # Abstract spec: what a correct exp/ln/pow should satisfy
  test/
    ExpProperty.t.sol           # Foundry fuzz tests vs PRBMath reference
    LnProperty.t.sol
    PowProperty.t.sol

Functions to include

Core (Phase 2a — first release)

Function	Spec	Algorithm	Error bound
exp(x)	e^x, WAD-scaled	Taylor series (20 terms) using mulDiv512	≤ 1 ULP
ln(x)	ln(x), WAD-scaled	log2(x) * ln(2) using Phase 1 log2	≤ 1 ULP
pow(base, exp)	base^exp, WAD-scaled	exp2(exp * log2(base))	≤ 2 ULP
wadMul(a, b)	a * b / WAD	mulDiv512(a, b, WAD)	exact
wadDiv(a, b)	a * WAD / b	mulDiv512(a, WAD, b)	exact (rounds down)
rayMul(a, b)	a * b / RAY	mulDiv512(a, b, RAY)	exact
rayDiv(a, b)	a * RAY / b	mulDiv512(a, RAY, b)	exact
wadToRay(x)	x * 10^9	multiplication, overflow-checked	exact
rayToWad(x)	x / 10^9	division, truncates	≤ 1 ray-unit

Extended (Phase 2b — second release)

Function	Spec	Use case
rpow(base, exp, scale)	(base/scale)^exp * scale	Compound interest (Aave-style)
compoundInterest(rate, time)	e^(rate * time)	Continuous compounding
geometricMean(a, b)	√(a * b)	AMM LP token pricing
inverseSqrt(x)	1 / √x	Concentrated liquidity
ceilDiv(a, b)	⌈a/b⌉	Share minting (round up to protect vault)

Proof strategy

Each function follows the same pattern:

1. Lean-level spec referencing Mathlib's Real.exp, Real.log, Real.sqrt, etc.
2. EDSL implementation using Phase 1 built-ins (mulDiv512, sqrt, exp2, log2) + loops (forEach, while)
3. Correctness proof: EDSL implementation agrees with Lean spec within stated error bound
4. Compilation correctness: inherited from Phase 1 built-in proofs + loop compilation proofs
5. Foundry differential tests: fuzz against PRBMath/Solmate reference implementations

Error bound proofs follow this shape:

theorem exp_error_bound (x : Uint256) (hx : x ≤ MAX_EXP_INPUT) :
  let r := exp x  -- EDSL-level execution
  let exact := Real.exp (x.toNat / WAD : ℝ) * WAD
  |r.toNat - Nat.round exact| ≤ 1

Why a separate package (not in verity core)

1. Separation of concerns: Core verity provides the EDSL + compiler + proof infrastructure. Math is a library concern.
2. Independent release cycle: Math functions can be added/improved without verity compiler releases.
3. User-extensible pattern: Other teams can create their own math packages (verity-math-bonding-curves, verity-math-options-pricing) following the same structure.
4. Build time: Mathlib-referencing proofs are compile-heavy. Keeping them out of the core build keeps verity fast.

Definition of done (Phase 2a)

• verity-math Lean package exists as a separate repo, builds against verity
• exp, ln, pow implemented and compile to correct Yul
• All three have Lean correctness proofs against Mathlib Real specs
• All three have proven error bounds (≤ N ULP, N stated explicitly)
• wadMul, wadDiv, rayMul, rayDiv, wadToRay, rayToWad implemented with exact-arithmetic proofs
• Foundry differential tests pass against PRBMath reference for all functions
• No sorry, no new axioms
• README with usage examples and proof guarantees
• Importable from any verity contract: import VerityMath.Functions.Exp

Definition of done (Phase 2b)

• rpow, compoundInterest, geometricMean, inverseSqrt, ceilDiv added
• All have correctness proofs and error bounds
• Differential tests against Aave/Solmate reference implementations

Dependencies

• Blocked by: Math: add mulDiv512, sqrt, exp2, log2 as compiler built-ins #1622 (Phase 1 math built-ins — mulDiv512, sqrt, exp2, log2)
• Blocked by: Language: fix forEach proof semantics + add while, break, continue #1623 (loop semantics fix — exp/ln Taylor series need working forEach/while)
• Enables: Phase 3 fixed-point type system (future issue)

Phase 3: Fixed-point type system (deferred, future issue)

Once Phase 2 is stable, a potential Phase 3 would add compile-time fixed-point types to the EDSL:

type WAD := FixedPoint Uint256 18
type RAY := FixedPoint Uint256 27

let price : WAD ← oracleRead ...
let shares : WAD ← wadDiv totalAssets price  -- compiler selects optimal Yul
let rayPrice : RAY ← wadToRay price          -- compiler inserts scaling

The compiler would:

• Type-check precision compatibility (can't add WAD + RAY without explicit conversion)
• Auto-insert scaling operations
• Select optimal Yul (shift for power-of-2 scales, mulDiv512 for arbitrary)
• Generate precision-preservation proof obligations

This is a significant compiler investment (3-6 months) and should only be pursued if Phase 2 adoption demonstrates demand. The Phase 2 library would become the implementation backend for Phase 3 types.