Example: ERC4626 Vault contract with share accounting proofs

[Th0rgal]

Why

ERC4626 (tokenized vault) is the #2 DeFi primitive after AMMs. Share-based accounting (deposit assets → mint shares, burn shares → withdraw assets) is used in lending protocols, yield aggregators, and staking contracts. Key properties:

• Share/asset exchange rate monotonicity
• Rounding correctness (no value leakage from rounding)
• Deposit/withdraw roundtrip bounds

This would complement the AMM example by demonstrating ratio-based arithmetic proofs.

Scope

Minimal vault with:

• deposit(assets) → mint shares proportional to assets/totalAssets
• withdraw(shares) → burn shares, return proportional assets
• totalAssets() / totalSupply() view functions

Key properties:

• Share price monotonicity: share price never decreases (absent external losses)
• Roundtrip bounds: withdraw(deposit(x)) returns at least x - 1 (rounding loss bounded)
• Conservation: totalAssets = sum of all depositor claims
• No inflation attack: prove first-depositor advantage is bounded (or mitigated by virtual shares)

Effort

2-3 weeks

Acceptance

• Vault contract defined with specs
• Core properties 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.

[Th0rgal]

I’m preparing a follow-up PR that lands a minimal Vault example as groundwork for this issue.

Scope of the PR:

• add Contracts/Vault/Vault.lean with a minimal ERC4626-style 1:1 asset/share model
• add a Solidity reference contract and unit tests
• wire the contract into compiler/test registries plus the differential-test interpreter surface

It does not attempt to close the full issue yet: proportional share pricing, roundtrip bounds, and the proof-complete ERC4626 accounting layer remain follow-up work.