Added more Move examples

Added the following examples to
`language/documentation/examples/experiment`:
- basic-coin: extracted from the Move tutorial
- coin-swap: Uniswap like contract in Move
- rounding-error: examples of verifying rounding errors using Prover
- math-puzzle: using Prover for fun

TODO:
- The next step is to add more document to the examples (e.g,
  README.md, code comments, ...).

Closes: aptos-labs#10099

language/documentation/examples/experimental/basic-coin/Move.toml

@@ -0,0 +1,9 @@
+[package]
+name = "BasicCoin"
+version = "0.0.0"
+
+[addresses]
+BasicCoin = "0xBC"
+
+[dependencies]
+MoveStdlib = { local = "../../../../move-stdlib/", addr_subst = { "Std" = "0x1" } }

language/documentation/examples/experimental/basic-coin/sources/BasicCoin.move

@@ -0,0 +1,150 @@
+/// This module defines a minimal and generic Coin and Balance.
+module BasicCoin::BasicCoin {
+    use Std::Errors;
+    use Std::Signer;
+
+    /// Error codes
+    const ENOT_MODULE_OWNER: u64 = 0;
+    const EINSUFFICIENT_BALANCE: u64 = 1;
+    const EALREADY_HAS_BALANCE: u64 = 2;
+    const EALREADY_INITIALIZED: u64 = 3;
+    const EEQUAL_ADDR: u64 = 4;
+
+    struct Coin<phantom CoinType> has store {
+        value: u64
+    }
+
+    struct Balance<phantom CoinType> has key {
+        coin: Coin<CoinType>
+    }
+
+    public fun publish_balance<CoinType>(account: &signer) {
+        let empty_coin = Coin<CoinType> { value: 0 };
+        assert!(!exists<Balance<CoinType>>(Signer::address_of(account)), Errors::already_published(EALREADY_HAS_BALANCE));
+        move_to(account, Balance<CoinType> { coin:  empty_coin });
+    }
+
+    spec publish_balance {
+        include Schema_publish<CoinType> {addr: Signer::address_of(account), amount: 0};
+    }
+
+    spec schema Schema_publish<CoinType> {
+        addr: address;
+        amount: u64;
+
+        aborts_if exists<Balance<CoinType>>(addr);
+
+        ensures exists<Balance<CoinType>>(addr);
+        let post balance_post = global<Balance<CoinType>>(addr).coin.value;
+
+        ensures balance_post == amount;
+    }
+
+    /// Mint `amount` tokens to `mint_addr`. This method requires a witness with `CoinType` so that the
+    /// module that owns `CoinType` can decide the minting policy.
+    public fun mint<CoinType: drop>(mint_addr: address, amount: u64, _witness: CoinType) acquires Balance {
+        // Deposit `amount` of tokens to mint_addr's balance
+        deposit(mint_addr, Coin<CoinType> { value: amount });
+    }
+
+    spec mint {
+        include DepositSchema<CoinType> {addr: mint_addr, amount};
+    }
+
+    /// Burn `amount` tokens from `burn_addr`. This method requires a witness with `CoinType` so that the
+    /// module that owns `CoinType` can decide the burning policy.
+    public fun burn<CoinType: drop>(burn_addr: address, amount: u64, _witness: CoinType) acquires Balance {
+        // Withdraw `amount` of tokens from mint_addr's balance
+        let Coin { value: _ } = withdraw<CoinType>(burn_addr, amount);
+    }
+
+    spec burn {
+        // TBD
+    }
+
+
+    public fun balance_of<CoinType>(owner: address): u64 acquires Balance {
+        borrow_global<Balance<CoinType>>(owner).coin.value
+    }
+
+    spec balance_of {
+        pragma aborts_if_is_strict;
+        aborts_if !exists<Balance<CoinType>>(owner);
+    }
+
+    /// Transfers `amount` of tokens from `from` to `to`. This method requires a witness with `CoinType` so that the
+    /// module that owns `CoinType` can decide the transferring policy.
+    public fun transfer<CoinType: drop>(from: &signer, to: address, amount: u64, _witness: CoinType) acquires Balance {
+        let from_addr = Signer::address_of(from);
+        assert!(from_addr != to, EEQUAL_ADDR);
+        let check = withdraw<CoinType>(from_addr, amount);
+        deposit<CoinType>(to, check);
+    }
+
+    spec transfer {
+        let addr_from = Signer::address_of(from);
+
+        let balance_from = global<Balance<CoinType>>(addr_from).coin.value;
+        let balance_to = global<Balance<CoinType>>(to).coin.value;
+        let post balance_from_post = global<Balance<CoinType>>(addr_from).coin.value;
+        let post balance_to_post = global<Balance<CoinType>>(to).coin.value;
+
+        aborts_if !exists<Balance<CoinType>>(addr_from);
+        aborts_if !exists<Balance<CoinType>>(to);
+        aborts_if balance_from < amount;
+        aborts_if balance_to + amount > MAX_U64;
+        aborts_if addr_from == to;
+
+        ensures balance_from_post == balance_from - amount;
+        ensures balance_to_post == balance_to + amount;
+    }
+
+    fun withdraw<CoinType>(addr: address, amount: u64) : Coin<CoinType> acquires Balance {
+        let balance = balance_of<CoinType>(addr);
+        assert!(balance >= amount, EINSUFFICIENT_BALANCE);
+        let balance_ref = &mut borrow_global_mut<Balance<CoinType>>(addr).coin.value;
+        *balance_ref = balance - amount;
+        Coin<CoinType> { value: amount }
+    }
+
+    spec withdraw {
+        let balance = global<Balance<CoinType>>(addr).coin.value;
+
+        aborts_if !exists<Balance<CoinType>>(addr);
+        aborts_if balance < amount;
+
+        let post balance_post = global<Balance<CoinType>>(addr).coin.value;
+        ensures result == Coin<CoinType> { value: amount };
+        ensures balance_post == balance - amount;
+    }
+
+    fun deposit<CoinType>(addr: address, check: Coin<CoinType>) acquires Balance{
+        let balance = balance_of<CoinType>(addr);
+        let balance_ref = &mut borrow_global_mut<Balance<CoinType>>(addr).coin.value;
+        let Coin { value } = check;
+        *balance_ref = balance + value;
+    }
+
+    spec deposit {
+        let balance = global<Balance<CoinType>>(addr).coin.value;
+        let check_value = check.value;
+
+        aborts_if !exists<Balance<CoinType>>(addr);
+        aborts_if balance + check_value > MAX_U64;
+
+        let post balance_post = global<Balance<CoinType>>(addr).coin.value;
+        ensures balance_post == balance + check_value;
+    }
+
+    spec schema DepositSchema<CoinType> {
+        addr: address;
+        amount: u64;
+        let balance = global<Balance<CoinType>>(addr).coin.value;
+
+        aborts_if !exists<Balance<CoinType>>(addr);
+        aborts_if balance + amount > MAX_U64;
+
+        let post balance_post = global<Balance<CoinType>>(addr).coin.value;
+        ensures balance_post == balance + amount;
+    }
+}

language/documentation/examples/experimental/coin-swap/Move.toml

@@ -0,0 +1,14 @@
+[package]
+name = "CoinSwap"
+version = "0.0.0"
+
+[addresses]
+Std = "0x1"
+CoinSwap = "0xC5"
+BasicCoin = "0xBC"
+GoldCoin = "0x9C"
+SilverCoin = "0x5C"
+
+[dependencies]
+MoveStdlib = { local = "../../../../move-stdlib" }
+BasicCoin = { local = "../basic-coin"}

language/documentation/examples/experimental/coin-swap/sources/CoinSwap.move

@@ -0,0 +1,109 @@
+module CoinSwap::CoinSwap {
+    use Std::Signer;
+    use Std::Errors;
+    use BasicCoin::BasicCoin;
+    use CoinSwap::PoolToken;
+
+    const ECOINSWAP_ADDRESS: u64 = 0;
+    const EPOOL: u64 = 0;
+
+    struct LiquidityPool<phantom CoinType1, phantom CoinType2> has key {
+        coin1: u64,
+        coin2: u64,
+        share: u64,
+    }
+
+    public fun create_pool<CoinType1: drop, CoinType2: drop>(
+        coinswap: &signer,
+        requester: &signer,
+        coin1: u64,
+        coin2: u64,
+        share: u64,
+        witness1: CoinType1,
+        witness2: CoinType2
+    ) {
+        // Create a pool at @CoinSwap.
+        // TODO: If the balance is already published, this step should be skipped rather than abort.
+        // TODO: Alternatively, `struct LiquidityPool` could be refactored to actually hold the coin (e.g., coin1: CoinType1).
+        BasicCoin::publish_balance<CoinType1>(coinswap);
+        BasicCoin::publish_balance<CoinType2>(coinswap);
+        assert!(Signer::address_of(coinswap) == @CoinSwap, Errors::invalid_argument(ECOINSWAP_ADDRESS));
+        assert!(!exists<LiquidityPool<CoinType1, CoinType2>>(Signer::address_of(coinswap)), Errors::already_published(EPOOL));
+        move_to(coinswap, LiquidityPool<CoinType1, CoinType2>{coin1, coin2, share});
+
+        // Transfer the initial liquidity of CoinType1 and CoinType2 to the pool under @CoinSwap.
+        BasicCoin::transfer<CoinType1>(requester, Signer::address_of(coinswap), coin1, witness1);
+        BasicCoin::transfer<CoinType2>(requester, Signer::address_of(coinswap), coin2, witness2);
+
+        // Mint PoolToken and deposit it in the account of requester.
+        PoolToken::setup_and_mint<CoinType1, CoinType2>(requester, share);
+    }
+
+    fun get_input_price(input_amount: u64, input_reserve: u64, output_reserve: u64): u64 {
+        let input_amount_with_fee = input_amount * 997;
+        let numerator = input_amount_with_fee * output_reserve;
+        let denominator = (input_reserve * 1000) + input_amount_with_fee;
+        numerator / denominator
+    }
+
+    public fun coin1_to_coin2_swap_input<CoinType1: drop, CoinType2: drop>(
+        coinswap: &signer,
+        requester: &signer,
+        coin1: u64,
+        witness1: CoinType1,
+        witness2: CoinType2
+    ) acquires LiquidityPool {
+        assert!(Signer::address_of(coinswap) == @CoinSwap, Errors::invalid_argument(ECOINSWAP_ADDRESS));
+        assert!(exists<LiquidityPool<CoinType1, CoinType2>>(Signer::address_of(coinswap)), Errors::not_published(EPOOL));
+        let pool = borrow_global_mut<LiquidityPool<CoinType1, CoinType2>>(Signer::address_of(coinswap));
+        let coin2 = get_input_price(coin1, pool.coin1, pool.coin2);
+        pool.coin1 = pool.coin1 + coin1;
+        pool.coin2 = pool.coin2 - coin2;
+
+        BasicCoin::transfer<CoinType1>(requester, Signer::address_of(coinswap), coin1, witness1);
+        BasicCoin::transfer<CoinType2>(coinswap, Signer::address_of(requester), coin2, witness2);
+    }
+
+    public fun add_liquidity<CoinType1: drop, CoinType2: drop>(
+        account: &signer,
+        coin1: u64,
+        coin2: u64,
+        witness1: CoinType1,
+        witness2: CoinType2,
+    ) acquires LiquidityPool {
+        let pool = borrow_global_mut<LiquidityPool<CoinType1, CoinType2>>(@CoinSwap);
+
+        let coin1_added = coin1;
+        let share_minted = (coin1_added * pool.share) / pool.coin1;
+        let coin2_added = (share_minted * pool.coin2) / pool.share;
+
+        pool.coin1 = pool.coin1 + coin1_added;
+        pool.coin2 = pool.coin2 + coin2_added;
+        pool.share = pool.share + share_minted;
+
+        BasicCoin::transfer<CoinType1>(account, @CoinSwap, coin1, witness1);
+        BasicCoin::transfer<CoinType2>(account, @CoinSwap, coin2, witness2);
+        PoolToken::mint<CoinType1, CoinType2>(Signer::address_of(account), share_minted)
+    }
+
+    public fun remove_liquidity<CoinType1: drop, CoinType2: drop>(
+        coinswap: &signer,
+        requester: &signer,
+        share: u64,
+        witness1: CoinType1,
+        witness2: CoinType2,
+    ) acquires LiquidityPool {
+        let pool = borrow_global_mut<LiquidityPool<CoinType1, CoinType2>>(@CoinSwap);
+
+        let coin1_removed = (pool.coin1 * share) / pool.share;
+        let coin2_removed = (pool.coin2 * share) / pool.share;
+
+        pool.coin1 = pool.coin1 - coin1_removed;
+        pool.coin2 = pool.coin2 - coin2_removed;
+        pool.share = pool.share - share;
+
+        BasicCoin::transfer<CoinType1>(coinswap, Signer::address_of(requester), coin1_removed, witness1);
+        BasicCoin::transfer<CoinType2>(coinswap, Signer::address_of(requester), coin2_removed, witness2);
+        PoolToken::burn<CoinType1, CoinType2>(Signer::address_of(requester), share)
+    }
+}

language/documentation/examples/experimental/coin-swap/sources/GoldCoin.move

@@ -0,0 +1,15 @@
+module GoldCoin::GoldCoin {
+    use Std::Signer;
+    use BasicCoin::BasicCoin;
+
+    struct GoldCoin has drop {}
+
+    public fun setup_and_mint(account: &signer, amount: u64) {
+        BasicCoin::publish_balance<GoldCoin>(account);
+        BasicCoin::mint<GoldCoin>(Signer::address_of(account), amount, GoldCoin{});
+    }
+
+    public fun transfer(from: &signer, to: address, amount: u64) {
+        BasicCoin::transfer<GoldCoin>(from, to, amount, GoldCoin {});
+    }
+}

language/documentation/examples/experimental/coin-swap/sources/PoolToken.move

@@ -0,0 +1,25 @@
+module CoinSwap::PoolToken {
+    use Std::Signer;
+    use BasicCoin::BasicCoin;
+
+    struct PoolToken<phantom CoinType1, phantom CoinType2> has drop {}
+
+    public fun setup_and_mint<CoinType1, CoinType2>(account: &signer, amount: u64) {
+        BasicCoin::publish_balance<PoolToken<CoinType1, CoinType2>>(account);
+        BasicCoin::mint<PoolToken<CoinType1, CoinType2>>(Signer::address_of(account), amount, PoolToken {});
+    }
+
+    public fun transfer<CoinType1, CoinType2>(from: &signer, to: address, amount: u64) {
+        BasicCoin::transfer<PoolToken<CoinType1, CoinType2>>(from, to, amount, PoolToken<CoinType1, CoinType2> {});
+    }
+
+    public fun mint<CoinType1, CoinType2>(mint_addr: address, amount: u64) {
+        // Deposit `total_value` amount of tokens to mint_addr's balance
+        BasicCoin::mint(mint_addr, amount, PoolToken<CoinType1, CoinType2> {});
+    }
+
+    public fun burn<CoinType1, CoinType2>(burn_addr: address, amount: u64) {
+        // Deposit `total_value` amount of tokens to mint_addr's balance
+        BasicCoin::burn(burn_addr, amount, PoolToken<CoinType1, CoinType2> {});
+    }
+}

language/documentation/examples/experimental/coin-swap/sources/SilverCoin.move

@@ -0,0 +1,15 @@
+module SilverCoin::SilverCoin {
+    use Std::Signer;
+    use BasicCoin::BasicCoin;
+
+    struct SilverCoin has drop {}
+
+    public fun setup_and_mint(account: &signer, amount: u64) {
+        BasicCoin::publish_balance<SilverCoin>(account);
+        BasicCoin::mint<SilverCoin>(Signer::address_of(account), amount, SilverCoin {});
+    }
+
+    public fun transfer(from: &signer, to: address, amount: u64) {
+        BasicCoin::transfer<SilverCoin>(from, to, amount, SilverCoin {});
+    }
+}

language/documentation/examples/experimental/rounding-error/Move.toml

@@ -0,0 +1,10 @@
+[package]
+name = "RoundingError"
+version = "0.0.0"
+
+[addresses]
+Std = "0x1"
+NamedAddr = "0xCAFE"
+
+[dependencies]
+MoveStdlib = { local = "../../../../move-stdlib" }