finance/options: fully collateralized options venue in Anchor v2, Anchor v1, and Quasar, with Kani proofs - #139
Open
mikemaccana wants to merge 3 commits into
Open
Conversation
Add an American, physically settled options venue in Anchor v2, Anchor v1 and Quasar, with a Kani proofs crate. A writer posts full collateral, the underlying for a call or the strike in the quote token for a put, and lists a lot with a premium and an expiry. A buyer pays the premium, the venue keeps a basis-point fee and the writer takes the rest. The holder may exercise any time before expiry, swapping the mirrored payment for the collateral; after expiry the writer reclaims it. Every amount is a product of contract-size integers, so no settlement path divides, and every handler asserts the custody ledger against the vault balances after its transfer. The design follows PsyOptions' fully collateralized model: no oracle, no margin, and no liquidation, so the only trust the venue asks for is the token program's. Each Anchor port carries 25 LiteSVM tests and the Quasar port 28, covering both lifecycles, the expiry boundary, every refusal, and the zero-fee case. The Kani crate proves the settlement amounts mirror across call and put, the premium split conserves the premium with an exact floor, the exercise and reclaim windows partition time, and the vault ledger returns to zero across every interleaving of two lots' lifecycles. Register the example in the workspace, the README, llms.txt, the changelog, and the Anchor and Kani workflows. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014RdEWCoCChaoKPhvcftHVG
Drop the comparison to a named options venue from the READMEs, the crate descriptions, the program doc comments, the repository README, llms.txt, and the changelog. The example stands on what it does: one account per lot, fully collateralized, physically settled. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014RdEWCoCChaoKPhvcftHVG
Use the same words as the book chapter. An option is the thing a writer lists and a holder buys, exercises, or lets expire; "lot" is the order book's quantity unit and meant something else two examples over, and "option account" named the account by its shape when every account is one. Comments, READMEs, changelogs, test doc comments, and the two variables in the ledger proof follow. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014RdEWCoCChaoKPhvcftHVG
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Adds
finance/options: an American, physically settled, fully collateralized options venue, in the three frameworks the other finance examples ship in, plus a Kani proofs crate. It is the companion to the book's new Options chapter.contractstimes a per-contract amount), so no settlement path divides. The only rounding is the floor in the fee split, which favors the writer.underlying_locked,quote_locked,fees_owed), and every handler that moves tokens asserts the vault balances still cover it (CustodyInvariantViolatedotherwise).Contents
finance/options/anchorfinance/options/anchor-v1finance/options/quasarfinance/options/kani-proofsThe Kani harnesses prove that physical settlement moves exactly the posted terms and mirrors across call and put, that the premium split conserves the premium with an exact floor, that the exercise and reclaim windows partition time, and that the vault ledger stays consistent across every interleaving of two options' lifecycles and returns to zero. The multiplied terms are bounded to 8 bits: with 16-bit operands the divider-versus-multiplier harnesses run for over 30 minutes, at 8 bits the whole suite finishes in about 70 seconds. The bounds and the reasoning are in the crate's README.
Wiring
Cargo.tomlworkspace member and regeneratedCargo.lock.README.mdandllms.txtentries, and aCHANGELOG.mdentry..github/workflows/anchor.yml: the v2 copy joins the--no-idllist (anchor#4947: theOptionKindandOptionStatusenums reach the IDL)..github/workflows/kani.yml: the proofs crate joins both matrices.Test plan
cargo testinfinance/options/anchor(25 pass),finance/options/anchor-v1(25 pass),finance/options/quasar(28 pass)cargo fmt --checkandcargo clippy --all-targets -- -D warningsin all four cratescargo kaniinfinance/options/kani-proofs: all four harnesses verified🤖 Generated with Claude Code
https://claude.ai/code/session_014RdEWCoCChaoKPhvcftHVG
Generated by Claude Code