neutrinomic/demo_sr9_dex

This repository is a demo of a decentralized exchange (a DEX, the kind of token-swapping smart contract popularised by Uniswap) written for the Internet Computer in the Motoko language. The author is very direct about what it is and is not. It is a research artifact meant to show off a verification technique called SR9; it is not audited, not production-ready, and absolutely not meant to hold real user funds. The DEX itself does the usual things a small AMM-style exchange does. Users deposit tokens from external ICRC-style ledgers (ICRC is the token standard on the Internet Computer, similar in spirit to ERC-20 on Ethereum) into a local balance held by the DEX. They can then swap one deposited token for another through constant-product liquidity pools, add or remove liquidity in those pools, and finally withdraw their balance back out to the external ledger. The fee on each swap is 0.3 percent, of which 20 percent goes to the operator and 80 percent stays in the pool for liquidity providers. A controller principal, which can be a human, an operations canister, or a DAO, is in charge of whitelisting ledgers, creating pools, and shutting things down safely. What makes this demo unusual is that the code carries machine-checked contracts. SR9 lowers those contracts to a verifier called Viper, which proves at compile time that certain properties always hold. The README lists the proven properties in detail. Deposits only credit a user after the underlying ledger transfer actually returns success. Withdrawals debit local balance before the external call and restore the exact amount if the call fails. Swaps recompute prices against current reserves rather than trusting a stale quote, cannot drain the output reserve, and respect a minimum-output limit. A central conservation equation, that the net amount on the external ledger equals what the DEX still owes users plus pending outflows plus officially abandoned dust, is preserved across every checked transition. A careful retirement flow lets a ledger be removed only after all pools, balances, and pending operations involving it have been cleared, with explicit user consent required for tiny dust amounts.