prop-amm: add oracle-quoted proprietary AMM example

[mikemaccana]

Adds finance/prop-amm: an oracle-quoted proprietary AMM — a market-making firm funds a market with its own capital and quotes both sides at the oracle price ± a spread. This is the Lifinity / SolFi / HumidiFi design that now fills most Solana swap volume via Jupiter routing, and it pairs with a new "The Prop AMM" chapter in the book (slotted after The Constant-Product AMM).

The teaching contrast with finance/token-swap: no curve, no liquidity providers, no pool shares (so no inflation attack — there is nothing to dilute), no price impact and nothing to sandwich (the price doesn't depend on the pool's balances). The risks move to stale quotes and adverse selection, which is where the design's oracle gates and set_quote pause live.

What's included

anchor/ — two-program workspace following the perpetual-futures template (prop-amm + mock-switchboard):

• initialize_market — pins pair, oracle feed, scale, spread, confidence limit; one market per pair (the deployment is the firm)
• deposit_inventory / withdraw_inventory — operator-only; withdrawal is unconditional, up to everything, because nobody else has a claim
• set_quote — re-spread or pull quotes (paused flag)
• swap — permissionless; ask = ceil(oracle × (1 + spread)), bid = floor(oracle × (1 − spread)), outputs floored (every rounding favors the market); gates for staleness (150 slots), confidence band, slippage minimum, inventory, pause; plus a post-math assert that output value never exceeds input value at the raw oracle price
• LiteSVM tests verify the math to the minor unit: at $165 with a 10 bps spread, 1,651.65 USDC buys exactly 10 NVDAx, selling them back returns exactly 1,648.35, and the 3.30 round trip is the whole fee. Every gate has a test proving it shuts.

quasar/ — port matching the Anchor design and math, with the feed injected as raw account bytes in tests (perps precedent). Note: quasar-svm is pinned to cb7565d — upstream HEAD (c63afd2, sbpf v3) moved to solana-program-runtime 4.1 / solana-address 2.6, which cannot co-resolve with the quasar-lang rev all the Quasar examples pin. The existing examples hit the same resolution failure on a fresh cargo resolve today; their next CI run against a changed lockfile will too, so the other eight Quasar examples may want the same pin as a follow-up.

kani-proofs/ — proves the quote brackets the oracle with exact roundings (over- and under-rounding both fail), the buy/sell oracle-value invariant (the swap handler's InvariantViolated assert can never fire while the math is intact), and that a round trip never profits the trader. Registered in both kani.yml matrices; plain unit tests pin the same numbers the LiteSVM tests and the book chapter use.

Also adds the Prop AMM section to the root README under Financial software.

Testing

• cargo check --tests clean (no warnings) for the Anchor workspace; cargo check --tests clean for the Quasar port; cargo test green in kani-proofs
• Full anchor build && cargo test runs in CI — the SBF toolchain isn't installable in my sandbox (network policy), so CI is the test gate, as with token-fundraiser: let a maker retire a failed raise and raise again #107
• All chapter/test numbers recomputed independently in Python

🤖 Generated with Claude Code

https://claude.ai/code/session_01MjDPoqwPYDGnLoMoXsto8r

---

Generated by Claude Code