From 4f4520c268b1a959735b8f38aa54138c8043406a Mon Sep 17 00:00:00 2001 From: Malcolm Langfield <35980963+langfield@users.noreply.github.com> Date: Fri, 3 Feb 2023 11:22:56 -0500 Subject: [PATCH 1/7] Add some working `toy_amm.cairo` variants --- tests/resources/golden/toy_amm/display.sh | 9 + tests/resources/golden/toy_amm/math.cairo | 65 +++++ .../golden/toy_amm/split_toy_amm.cairo | 217 +++++++++++++++ ..._amm_with_split_and_original_do_swap.cairo | 257 ++++++++++++++++++ 4 files changed, 548 insertions(+) create mode 100755 tests/resources/golden/toy_amm/display.sh create mode 100644 tests/resources/golden/toy_amm/math.cairo create mode 100644 tests/resources/golden/toy_amm/split_toy_amm.cairo create mode 100644 tests/resources/golden/toy_amm/toy_amm_with_split_and_original_do_swap.cairo diff --git a/tests/resources/golden/toy_amm/display.sh b/tests/resources/golden/toy_amm/display.sh new file mode 100755 index 00000000..b4e2bf0d --- /dev/null +++ b/tests/resources/golden/toy_amm/display.sh @@ -0,0 +1,9 @@ +#!/bin/bash +echo '~~~~~~~~~~~~~~~{SOURCE}~~~~~~~~~~~~~~' \ + && cat $1 && echo '' \ + && echo '~~~~~~~~~~~~~~{RESULT}~~~~~~~~~~~~~~~' \ + && horus-compile $1 --output a.json --spec_output b.json && horus-check -s z3 -s mathsat -t 5000 a.json b.json \ + && echo '~~~~~~~~~~~~~~{REVISION}~~~~~~~~~~~~~' \ + && git log --oneline -n 1 && echo '' \ + && echo '~~~~~~~~~~~~~~{FILENAME}~~~~~~~~~~~~~' \ + && echo $1 diff --git a/tests/resources/golden/toy_amm/math.cairo b/tests/resources/golden/toy_amm/math.cairo new file mode 100644 index 00000000..71a34c81 --- /dev/null +++ b/tests/resources/golden/toy_amm/math.cairo @@ -0,0 +1,65 @@ +// Verifies that a >= 0 (or more precisely 0 <= a < RANGE_CHECK_BOUND). +// @post 0 <= a and a < 2**128 +func assert_nn{range_check_ptr}(a) { + %{ + from starkware.cairo.common.math_utils import assert_integer + assert_integer(ids.a) + assert 0 <= ids.a % PRIME < range_check_builtin.bound, f'a = {ids.a} is out of range.' + %} + a = [range_check_ptr]; + let range_check_ptr = range_check_ptr + 1; + return (); +} + +// Verifies that a <= b (or more precisely 0 <= b - a < RANGE_CHECK_BOUND). +// @post 0 <= b - a and b - a < 2**128 +func assert_le{range_check_ptr}(a, b) { + assert_nn(b - a); + return (); +} + +// Verifies that 0 <= a <= b. +// +// Prover assumption: b < RANGE_CHECK_BOUND. +// +// This function is still sound without the prover assumptions. In that case, it is guaranteed +// that a < RANGE_CHECK_BOUND and b < 2 * RANGE_CHECK_BOUND. +// @pre b < 2**128 +// @post 0 <= a and a <= b +func assert_nn_le{range_check_ptr}(a, b) { + assert_nn(a); + assert_le(a, b); + return (); +} + +// Returns q and r such that: +// 0 <= q < rc_bound, 0 <= r < div and value = q * div + r. +// +// Assumption: 0 < div <= PRIME / rc_bound. +// Prover assumption: value / div < rc_bound. +// +// The value of div is restricted to make sure there is no overflow. +// q * div + r < (q + 1) * div <= rc_bound * (PRIME / rc_bound) = PRIME. +// +// @pre 0 < div +// @pre div <= 10633823966279326983230456482242756608 +// @pre value < 2**128 * div +// @post 0 <= $Return.q and $Return.q < 2**128 +// @post 0 <= $Return.r and $Return.r < div +// @post value == $Return.q * div + $Return.r +func unsigned_div_rem{range_check_ptr}(value, div) -> (q: felt, r: felt) { + let r = [range_check_ptr]; + let q = [range_check_ptr + 1]; + let range_check_ptr = range_check_ptr + 2; + %{ + from starkware.cairo.common.math_utils import assert_integer + assert_integer(ids.div) + assert 0 < ids.div <= PRIME // range_check_builtin.bound, \ + f'div={hex(ids.div)} is out of the valid range.' + ids.q, ids.r = divmod(ids.value, ids.div) + %} + assert_le(r, div - 1); + + assert value = q * div + r; + return (q, r); +} diff --git a/tests/resources/golden/toy_amm/split_toy_amm.cairo b/tests/resources/golden/toy_amm/split_toy_amm.cairo new file mode 100644 index 00000000..0c978a72 --- /dev/null +++ b/tests/resources/golden/toy_amm/split_toy_amm.cairo @@ -0,0 +1,217 @@ +%lang starknet + +%builtins pedersen +from starkware.cairo.common.cairo_builtins import HashBuiltin + +from starkware.cairo.common.hash import hash2 + +from math import assert_le, assert_nn_le, unsigned_div_rem +// The maximum amount of each token that belongs to the AMM. + +const BALANCE_UPPER_BOUND = 2 ** 64; +const TOKEN_TYPE_A = 1; +const TOKEN_TYPE_B = 2; + +// Ensure the user's balances are much smaller than the pool's balance. + +const POOL_UPPER_BOUND = 2 ** 30; + +const ACCOUNT_BALANCE_BOUND = 1073741; // 2**30 // 1000. + +// A map from account and token type to the corresponding balance of that account. + +@storage_var + +func account_balance(account_id: felt, token_type: felt) -> (balance: felt) { + +} + +// A map from token type to the corresponding balance of the pool. + +@storage_var + +func pool_balance(token_type: felt) -> (balance: felt) { + +} + +// Adds amount to the account's balance for the given token. + +// amount may be positive or negative. + +// Assert before setting that the balance does not exceed the upper bound. + +// + +// @storage_update account_balance(account_id, token_type) := account_balance(account_id, token_type) + amount + +func modify_account_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( + + account_id: felt, token_type: felt, amount: felt + +) { + + let (current_balance) = account_balance.read(account_id, token_type); + + tempvar new_balance = current_balance + amount; + + assert_nn_le(new_balance, BALANCE_UPPER_BOUND - 1); + + account_balance.write(account_id=account_id, token_type=token_type, value=new_balance); + + return (); + +} + +// Returns the account's balance for the given token. + +// + +// @post $Return.balance == account_balance(account_id, token_type) + +func get_account_token_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( + + account_id: felt, token_type: felt + +) -> (balance: felt) { + + return account_balance.read(account_id, token_type); + +} + +// Sets the pool's balance for the given token. +// Asserts before setting that the balance does not exceed the upper bound. +// +// @storage_update pool_balance(token_type) := balance + +func set_pool_token_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( + + token_type: felt, balance: felt + +) { + + assert_nn_le(balance, BALANCE_UPPER_BOUND - 1); + + pool_balance.write(token_type, balance); + + return (); + +} + +// Returns the pool's balance. +// @post $Return.balance == pool_balance(token_type) +func get_pool_token_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( + + token_type: felt + +) -> (balance: felt) { + + return pool_balance.read(token_type); + +} + +// Swaps tokens between the given account and the pool. +// +// @declare $old_pool_balance_from: felt +// @declare $old_pool_balance_to: felt +// @pre pool_balance(token_from) == $old_pool_balance_from +// @pre pool_balance(token_to) == $old_pool_balance_to +// +// Tokens should be different +// @pre (token_from == TOKEN_TYPE_A and token_to == TOKEN_TYPE_B) +// +// The account has enough balance +// @pre 0 < amount_from and amount_from <= account_balance(account_id, token_from) +// +// The pool balances are positive +// @pre pool_balance(token_to) >= 0 +// @pre pool_balance(token_from) >= 0 +// +// Assumptions needed for unsigned_div_rem to not overflow +// @pre pool_balance(token_from) + amount_from <= 10633823966279326983230456482242756608 +// @pre pool_balance(token_to) * amount_from < 2**128 * (pool_balance(token_from) + amount_from) +// +// The returned amount_to is correct. +// @post $Return.amm_from_balance == pool_balance(token_from) +// @post $Return.amm_to_balance == pool_balance(token_to) +// @post $old_pool_balance_to * amount_from == $Return.amount_to * ($old_pool_balance_from + amount_from) + $Return.r +// The pool balances are positive +// @post $Return.amm_to_balance >= 0 +// @post $Return.amm_from_balance >= 0 +func do_swap_lets{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( + account_id: felt, token_from: felt, token_to: felt, amount_from: felt +) -> (amm_from_balance: felt, amm_to_balance: felt, amount_to: felt, r: felt) { + alloc_locals; + // Get pool balance. + let (local amm_from_balance) = get_pool_token_balance(token_type=token_from); + let (local amm_to_balance) = get_pool_token_balance(token_type=token_to); + // Calculate swap amount. + let (local amount_to, local r) = unsigned_div_rem( + amm_to_balance * amount_from, amm_from_balance + amount_from + ); + return (amm_from_balance=amm_from_balance, amm_to_balance=amm_to_balance, amount_to=amount_to, r=r); +} +// Swaps tokens between the given account and the pool. +// +// Pool balance is updated +// @storage_update pool_balance(token_from) := amm_from_balance + amount_from +// +// Account balance is updated +// @storage_update account_balance(account_id, token_from) := account_balance(account_id, token_from) - amount_from +func do_swap_from_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( + account_id: felt, token_from: felt, amount_from: felt, amm_from_balance: felt, +) -> () { + // Update token_from balances. + modify_account_balance(account_id=account_id, token_type=token_from, amount=-amount_from); + set_pool_token_balance(token_type=token_from, balance=amm_from_balance + amount_from); + return (); + +} +// Swaps tokens between the given account and the pool. +// +// Pool balance is updated +// @storage_update pool_balance(token_to) := amm_to_balance - amount_to +// +// Account balance is updated +// @storage_update account_balance(account_id, token_to) := account_balance(account_id, token_to) + amount_to +func do_swap_to_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( + account_id: felt, token_to: felt, amount_to: felt, amm_to_balance: felt, +) -> () { + // Update token_to balances. + modify_account_balance(account_id=account_id, token_type=token_to, amount=amount_to); + set_pool_token_balance(token_type=token_to, balance=amm_to_balance - amount_to); + return (); +} + +// @post (token_type == TOKEN_TYPE_A and $Return.t == TOKEN_TYPE_B) or (token_type != TOKEN_TYPE_A and $Return.t == TOKEN_TYPE_A) +func get_opposite_token(token_type: felt) -> (t: felt) { + if (token_type == TOKEN_TYPE_A) { + return (TOKEN_TYPE_B,); + } else { + return (TOKEN_TYPE_A,); + } +} +// Adds demo tokens to the given account. +// @storage_update account_balance(account_id, TOKEN_TYPE_A) := account_balance(account_id, TOKEN_TYPE_A) + token_a_amount +// @storage_update account_balance(account_id, TOKEN_TYPE_B) := account_balance(account_id, TOKEN_TYPE_B) + token_b_amount +func add_demo_token{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( + account_id: felt, token_a_amount: felt, token_b_amount: felt +) { + // Make sure the account's balance is much smaller then pool init balance. + assert_nn_le(token_a_amount, ACCOUNT_BALANCE_BOUND - 1); + assert_nn_le(token_b_amount, ACCOUNT_BALANCE_BOUND - 1); + modify_account_balance(account_id=account_id, token_type=TOKEN_TYPE_A, amount=token_a_amount); + modify_account_balance(account_id=account_id, token_type=TOKEN_TYPE_B, amount=token_b_amount); + return (); +} +// Until we have LPs, for testing, we'll need to initialize the AMM somehow. +// @storage_update pool_balance(TOKEN_TYPE_A) := token_a +// @storage_update pool_balance(TOKEN_TYPE_B) := token_b +func init_pool{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( + token_a: felt, token_b: felt +) { + assert_nn_le(token_a, POOL_UPPER_BOUND - 1); + assert_nn_le(token_b, POOL_UPPER_BOUND - 1); + set_pool_token_balance(token_type=TOKEN_TYPE_A, balance=token_a); + set_pool_token_balance(token_type=TOKEN_TYPE_B, balance=token_b); + return (); +} \ No newline at end of file diff --git a/tests/resources/golden/toy_amm/toy_amm_with_split_and_original_do_swap.cairo b/tests/resources/golden/toy_amm/toy_amm_with_split_and_original_do_swap.cairo new file mode 100644 index 00000000..7ea1f7b0 --- /dev/null +++ b/tests/resources/golden/toy_amm/toy_amm_with_split_and_original_do_swap.cairo @@ -0,0 +1,257 @@ +%lang starknet + +%builtins pedersen +from starkware.cairo.common.cairo_builtins import HashBuiltin + +from starkware.cairo.common.hash import hash2 + +from math import assert_le, assert_nn_le, unsigned_div_rem +// The maximum amount of each token that belongs to the AMM. + +const BALANCE_UPPER_BOUND = 2 ** 64; +const TOKEN_TYPE_A = 1; +const TOKEN_TYPE_B = 2; + +// Ensure the user's balances are much smaller than the pool's balance. + +const POOL_UPPER_BOUND = 2 ** 30; + +const ACCOUNT_BALANCE_BOUND = 1073741; // 2**30 // 1000. + +// A map from account and token type to the corresponding balance of that account. + +@storage_var + +func account_balance(account_id: felt, token_type: felt) -> (balance: felt) { + +} + +// A map from token type to the corresponding balance of the pool. + +@storage_var + +func pool_balance(token_type: felt) -> (balance: felt) { + +} + +// Adds amount to the account's balance for the given token. + +// amount may be positive or negative. + +// Assert before setting that the balance does not exceed the upper bound. + +// + +// @storage_update account_balance(account_id, token_type) := account_balance(account_id, token_type) + amount + +func modify_account_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( + + account_id: felt, token_type: felt, amount: felt + +) { + + let (current_balance) = account_balance.read(account_id, token_type); + + tempvar new_balance = current_balance + amount; + + assert_nn_le(new_balance, BALANCE_UPPER_BOUND - 1); + + account_balance.write(account_id=account_id, token_type=token_type, value=new_balance); + + return (); + +} + +// Returns the account's balance for the given token. + +// + +// @post $Return.balance == account_balance(account_id, token_type) + +func get_account_token_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( + + account_id: felt, token_type: felt + +) -> (balance: felt) { + + return account_balance.read(account_id, token_type); + +} + +// Sets the pool's balance for the given token. +// Asserts before setting that the balance does not exceed the upper bound. +// +// @storage_update pool_balance(token_type) := balance + +func set_pool_token_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( + + token_type: felt, balance: felt + +) { + + assert_nn_le(balance, BALANCE_UPPER_BOUND - 1); + + pool_balance.write(token_type, balance); + + return (); + +} + +// Returns the pool's balance. +// @post $Return.balance == pool_balance(token_type) +func get_pool_token_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( + + token_type: felt + +) -> (balance: felt) { + + return pool_balance.read(token_type); + +} + +// Swaps tokens between the given account and the pool. +// +// @declare $old_pool_balance_from: felt +// @declare $old_pool_balance_to: felt +// @pre pool_balance(token_from) == $old_pool_balance_from +// @pre pool_balance(token_to) == $old_pool_balance_to +// +// Tokens should be different +// @pre (token_from == TOKEN_TYPE_A and token_to == TOKEN_TYPE_B) +// +// The account has enough balance +// @pre 0 < amount_from and amount_from <= account_balance(account_id, token_from) +// +// The pool balances are positive +// @pre pool_balance(token_to) >= 0 +// @pre pool_balance(token_from) >= 0 +// +// Assumptions needed for unsigned_div_rem to not overflow +// @pre pool_balance(token_from) + amount_from <= 10633823966279326983230456482242756608 +// @pre pool_balance(token_to) * amount_from < 2**128 * (pool_balance(token_from) + amount_from) +// +// The returned amount_to is correct. +// @post $Return.amm_from_balance == pool_balance(token_from) +// @post $Return.amm_to_balance == pool_balance(token_to) +// @post $old_pool_balance_to * amount_from == $Return.amount_to * ($old_pool_balance_from + amount_from) + $Return.r +// The pool balances are positive +// @post $Return.amm_to_balance >= 0 +// @post $Return.amm_from_balance >= 0 +func do_swap_lets{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( + account_id: felt, token_from: felt, token_to: felt, amount_from: felt +) -> (amm_from_balance: felt, amm_to_balance: felt, amount_to: felt, r: felt) { + alloc_locals; + // Get pool balance. + let (local amm_from_balance) = get_pool_token_balance(token_type=token_from); + let (local amm_to_balance) = get_pool_token_balance(token_type=token_to); + // Calculate swap amount. + let (local amount_to, local r) = unsigned_div_rem( + amm_to_balance * amount_from, amm_from_balance + amount_from + ); + return (amm_from_balance=amm_from_balance, amm_to_balance=amm_to_balance, amount_to=amount_to, r=r); +} +// Swaps tokens between the given account and the pool. +// +// Pool balance is updated +// @storage_update pool_balance(token_from) := amm_from_balance + amount_from +// +// Account balance is updated +// @storage_update account_balance(account_id, token_from) := account_balance(account_id, token_from) - amount_from +func do_swap_from_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( + account_id: felt, token_from: felt, amount_from: felt, amm_from_balance: felt, +) -> () { + // Update token_from balances. + modify_account_balance(account_id=account_id, token_type=token_from, amount=-amount_from); + set_pool_token_balance(token_type=token_from, balance=amm_from_balance + amount_from); + return (); + +} +// Swaps tokens between the given account and the pool. +// +// Pool balance is updated +// @storage_update pool_balance(token_to) := amm_to_balance - amount_to +// +// Account balance is updated +// @storage_update account_balance(account_id, token_to) := account_balance(account_id, token_to) + amount_to +func do_swap_to_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( + account_id: felt, token_to: felt, amount_to: felt, amm_to_balance: felt, +) -> () { + // Update token_to balances. + modify_account_balance(account_id=account_id, token_type=token_to, amount=amount_to); + set_pool_token_balance(token_type=token_to, balance=amm_to_balance - amount_to); + return (); +} + +// Swaps tokens between the given account and the pool. +// +// @declare $old_pool_balance_from: felt +// @declare $old_pool_balance_to: felt +// @pre pool_balance(token_from) == $old_pool_balance_from +// @pre pool_balance(token_to) == $old_pool_balance_to +// +// Tokens should be different +// @pre (token_from == TOKEN_TYPE_A and token_to == TOKEN_TYPE_B) +// +// The account has enough balance +// @pre 0 < amount_from and amount_from <= account_balance(account_id, token_from) +// +// The pool balances are positive +// @pre pool_balance(token_to) >= 0 +// @pre pool_balance(token_from) >= 0 +// +// Assumptions needed for unsigned_div_rem to not overflow +// @pre pool_balance(token_from) + amount_from <= 10633823966279326983230456482242756608 +// @pre pool_balance(token_to) * amount_from < 2**128 * (pool_balance(token_from) + amount_from) +// +// Pool balance is updated +// @storage_update pool_balance(token_from) := pool_balance(token_from) + amount_from +// @storage_update pool_balance(token_to) := pool_balance(token_to) - $Return.amount_to +// +// Account balance is updated +// @storage_update account_balance(account_id, token_from) := account_balance(account_id, token_from) - amount_from +// @storage_update account_balance(account_id, token_to) := account_balance(account_id, token_to) + $Return.amount_to +// +// The returned amount_to is correct. +// @post $old_pool_balance_to * amount_from == $Return.amount_to * ($old_pool_balance_from + amount_from) + $Return.r +func do_swap{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( + account_id: felt, token_from: felt, token_to: felt, amount_from: felt +) -> (amount_to: felt, r: felt) { + let (amm_from_balance, amm_to_balance, amount_to, r) = do_swap_lets(account_id, token_from, token_to, amount_from); + do_swap_from_balance(account_id, token_from, amount_from, amm_from_balance); + do_swap_to_balance(account_id, token_to, amount_to, amm_to_balance); + return (amount_to=amount_to, r=r); +} + +// @post (token_type == TOKEN_TYPE_A and $Return.t == TOKEN_TYPE_B) or (token_type != TOKEN_TYPE_A and $Return.t == TOKEN_TYPE_A) +func get_opposite_token(token_type: felt) -> (t: felt) { + if (token_type == TOKEN_TYPE_A) { + return (TOKEN_TYPE_B,); + } else { + return (TOKEN_TYPE_A,); + } +} +// Adds demo tokens to the given account. +// @storage_update account_balance(account_id, TOKEN_TYPE_A) := account_balance(account_id, TOKEN_TYPE_A) + token_a_amount +// @storage_update account_balance(account_id, TOKEN_TYPE_B) := account_balance(account_id, TOKEN_TYPE_B) + token_b_amount +func add_demo_token{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( + account_id: felt, token_a_amount: felt, token_b_amount: felt +) { + // Make sure the account's balance is much smaller then pool init balance. + assert_nn_le(token_a_amount, ACCOUNT_BALANCE_BOUND - 1); + assert_nn_le(token_b_amount, ACCOUNT_BALANCE_BOUND - 1); + modify_account_balance(account_id=account_id, token_type=TOKEN_TYPE_A, amount=token_a_amount); + modify_account_balance(account_id=account_id, token_type=TOKEN_TYPE_B, amount=token_b_amount); + return (); +} +// Until we have LPs, for testing, we'll need to initialize the AMM somehow. +// @storage_update pool_balance(TOKEN_TYPE_A) := token_a +// @storage_update pool_balance(TOKEN_TYPE_B) := token_b +func init_pool{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( + token_a: felt, token_b: felt +) { + assert_nn_le(token_a, POOL_UPPER_BOUND - 1); + assert_nn_le(token_b, POOL_UPPER_BOUND - 1); + set_pool_token_balance(token_type=TOKEN_TYPE_A, balance=token_a); + set_pool_token_balance(token_type=TOKEN_TYPE_B, balance=token_b); + return (); +} \ No newline at end of file From e59cac2747dcf1296ca82d2aeb9b353c88bd07d0 Mon Sep 17 00:00:00 2001 From: Julian Sutherland Date: Sun, 5 Feb 2023 00:54:22 +0000 Subject: [PATCH 2/7] Fixed bug that removed MathSAT from solver list globally rather than locally for a module for which it is inappropriate --- src/Horus/Global.hs | 19 +- tests/resources/golden/toy_amm_split.cairo | 261 +++++++++++++++++++++ tests/resources/golden/toy_amm_split.gold | 44 ++++ 3 files changed, 317 insertions(+), 7 deletions(-) create mode 100644 tests/resources/golden/toy_amm_split.cairo create mode 100644 tests/resources/golden/toy_amm_split.gold diff --git a/src/Horus/Global.hs b/src/Horus/Global.hs index 612cafaa..127cc7e7 100644 --- a/src/Horus/Global.hs +++ b/src/Horus/Global.hs @@ -192,12 +192,11 @@ mkLabeledFuncName qualifiedFuncName labelsSummary = qualifiedFuncName <> "." <> solveModule :: Module -> GlobalL SolvingInfo solveModule m = do inlinables <- getInlinables - checkMathsat m identifiers <- getIdentifiers let (qualifiedFuncName, labelsSummary, oracleSuffix) = getModuleNameParts identifiers m moduleName = mkLabeledFuncName qualifiedFuncName labelsSummary <> oracleSuffix inlinable = m_calledF m `elem` Set.map sf_pc inlinables - result <- mkResult moduleName + result <- removeMathSAT m (mkResult moduleName) pure SolvingInfo{si_moduleName = moduleName, si_funcName = qualifiedFuncName, si_result = result, si_inlinable = inlinable} where mkResult :: Text -> GlobalL HorusResult @@ -242,16 +241,22 @@ writeSmtQueries queries dir moduleName = do newFileName n = dir "optimized_goals_" <> unpack moduleName show n <> ".smt2" writeQueryFile (n, q) = writeFile' (newFileName n) q -checkMathsat :: Module -> GlobalL () -checkMathsat m = do +removeMathSAT :: Module -> GlobalL a -> GlobalL a +removeMathSAT m run = do conf <- getConfig let solver = cfg_solver conf usesLvars <- or <$> traverse instUsesLvars (m_prog m) - when (includesMathsat solver && usesLvars) $ do + if (includesMathsat solver && usesLvars) + then do let solver' = filterMathsat solver if isEmptySolver solver' - then throw "MathSat solver was used to analyze a call with a logical variable in its specification." - else setConfig conf{cfg_solver = solver'} + then throw "Only the MathSAT solver was used to analyze a call with a logical variable in its specification." + else do + setConfig conf{cfg_solver = solver'} + result <- run + setConfig conf + pure result + else run where -- FIXME should check not just pre, but also post instUsesLvars i = falseIfError $ do diff --git a/tests/resources/golden/toy_amm_split.cairo b/tests/resources/golden/toy_amm_split.cairo new file mode 100644 index 00000000..c3960d6f --- /dev/null +++ b/tests/resources/golden/toy_amm_split.cairo @@ -0,0 +1,261 @@ +%lang starknet + +%builtins pedersen +from starkware.cairo.common.cairo_builtins import HashBuiltin + +from starkware.cairo.common.hash import hash2 + +from math import assert_le, assert_nn_le, unsigned_div_rem +// The maximum amount of each token that belongs to the AMM. + +const BALANCE_UPPER_BOUND = 2 ** 64; +const TOKEN_TYPE_A = 1; +const TOKEN_TYPE_B = 2; + +// Ensure the user's balances are much smaller than the pool's balance. + +const POOL_UPPER_BOUND = 2 ** 30; + +const ACCOUNT_BALANCE_BOUND = 1073741; // 2**30 // 1000. + +// A map from account and token type to the corresponding balance of that account. + +@storage_var + +func account_balance(account_id: felt, token_type: felt) -> (balance: felt) { + +} + +// A map from token type to the corresponding balance of the pool. + +@storage_var + +func pool_balance(token_type: felt) -> (balance: felt) { + +} + +// Adds amount to the account's balance for the given token. + +// amount may be positive or negative. + +// Assert before setting that the balance does not exceed the upper bound. + +// + +// @storage_update account_balance(account_id, token_type) := account_balance(account_id, token_type) + amount + +func modify_account_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( + + account_id: felt, token_type: felt, amount: felt + +) { + + let (current_balance) = account_balance.read(account_id, token_type); + + tempvar new_balance = current_balance + amount; + + assert_nn_le(new_balance, BALANCE_UPPER_BOUND - 1); + + account_balance.write(account_id=account_id, token_type=token_type, value=new_balance); + + return (); + +} + +// Returns the account's balance for the given token. + +// + +// @post $Return.balance == account_balance(account_id, token_type) + +func get_account_token_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( + + account_id: felt, token_type: felt + +) -> (balance: felt) { + + return account_balance.read(account_id, token_type); + +} + +// Sets the pool's balance for the given token. +// Asserts before setting that the balance does not exceed the upper bound. +// +// @storage_update pool_balance(token_type) := balance + +func set_pool_token_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( + + token_type: felt, balance: felt + +) { + + assert_nn_le(balance, BALANCE_UPPER_BOUND - 1); + + pool_balance.write(token_type, balance); + + return (); + +} + +// Returns the pool's balance. +// @post $Return.balance == pool_balance(token_type) +func get_pool_token_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( + + token_type: felt + +) -> (balance: felt) { + + return pool_balance.read(token_type); + +} + +// Swaps tokens between the given account and the pool. +// +// @declare $old_pool_balance_from: felt +// @declare $old_pool_balance_to: felt +// @pre pool_balance(token_from) == $old_pool_balance_from +// @pre pool_balance(token_to) == $old_pool_balance_to +// +// Tokens should be different +// @pre (token_from == TOKEN_TYPE_A and token_to == TOKEN_TYPE_B) +// +// The account has enough balance +// @pre 0 < amount_from and amount_from <= account_balance(account_id, token_from) +// +// The pool balances are positive +// @pre pool_balance(token_to) >= 0 +// @pre pool_balance(token_from) >= 0 +// +// Assumptions needed for unsigned_div_rem to not overflow +// @pre pool_balance(token_from) + amount_from <= 10633823966279326983230456482242756608 +// @pre pool_balance(token_to) * amount_from < 2**128 * (pool_balance(token_from) + amount_from) +// +// The returned amount_to is correct. +// @post $Return.amm_from_balance == pool_balance(token_from) +// @post $Return.amm_to_balance == pool_balance(token_to) +// @post $old_pool_balance_to * amount_from == $Return.amount_to * ($old_pool_balance_from + amount_from) + $Return.r +// The pool balances are positive +// @post $Return.amm_to_balance >= 0 +// @post $Return.amm_from_balance >= 0 +func do_swap_lets{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( + account_id: felt, token_from: felt, token_to: felt, amount_from: felt +) -> (amm_from_balance: felt, amm_to_balance: felt, amount_to: felt, r: felt) { + alloc_locals; + // Get pool balance. + let (local amm_from_balance) = get_pool_token_balance(token_type=token_from); + let (local amm_to_balance) = get_pool_token_balance(token_type=token_to); + // Calculate swap amount. + let (local amount_to, local r) = unsigned_div_rem( + amm_to_balance * amount_from, amm_from_balance + amount_from + ); + return (amm_from_balance=amm_from_balance, amm_to_balance=amm_to_balance, amount_to=amount_to, r=r); +} + +// Swaps tokens between the given account and the pool. +// +// Pool balance is updated +// @storage_update pool_balance(token_from) := amm_from_balance + amount_from +// +// Account balance is updated +// @storage_update account_balance(account_id, token_from) := account_balance(account_id, token_from) - amount_from +func do_swap_from_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( + account_id: felt, token_from: felt, amount_from: felt, amm_from_balance: felt, +) -> () { + // Update token_from balances. + modify_account_balance(account_id=account_id, token_type=token_from, amount=-amount_from); + set_pool_token_balance(token_type=token_from, balance=amm_from_balance + amount_from); + return (); + +} + +// Swaps tokens between the given account and the pool. +// +// Pool balance is updated +// @storage_update pool_balance(token_to) := amm_to_balance - amount_to +// +// Account balance is updated +// @storage_update account_balance(account_id, token_to) := account_balance(account_id, token_to) + amount_to +func do_swap_to_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( + account_id: felt, token_to: felt, amount_to: felt, amm_to_balance: felt, +) -> () { + // Update token_to balances. + modify_account_balance(account_id=account_id, token_type=token_to, amount=amount_to); + set_pool_token_balance(token_type=token_to, balance=amm_to_balance - amount_to); + return (); +} + +// Swaps tokens between the given account and the pool. +// +// @declare $old_pool_balance_from: felt +// @declare $old_pool_balance_to: felt +// @pre pool_balance(token_from) == $old_pool_balance_from +// @pre pool_balance(token_to) == $old_pool_balance_to +// +// Tokens should be different +// @pre (token_from == TOKEN_TYPE_A and token_to == TOKEN_TYPE_B) +// +// The account has enough balance +// @pre 0 < amount_from and amount_from <= account_balance(account_id, token_from) +// +// The pool balances are positive +// @pre pool_balance(token_to) >= 0 +// @pre pool_balance(token_from) >= 0 +// +// Assumptions needed for unsigned_div_rem to not overflow +// @pre pool_balance(token_from) + amount_from <= 10633823966279326983230456482242756608 +// @pre pool_balance(token_to) * amount_from < 2**128 * (pool_balance(token_from) + amount_from) +// +// Pool balance is updated +// @storage_update pool_balance(token_from) := pool_balance(token_from) + amount_from +// @storage_update pool_balance(token_to) := pool_balance(token_to) - $Return.amount_to +// +// Account balance is updated +// @storage_update account_balance(account_id, token_from) := account_balance(account_id, token_from) - amount_from +// @storage_update account_balance(account_id, token_to) := account_balance(account_id, token_to) + $Return.amount_to +// +// The returned amount_to is correct. +// @post $old_pool_balance_to * amount_from == $Return.amount_to * ($old_pool_balance_from + amount_from) + $Return.r +func do_swap{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( + account_id: felt, token_from: felt, token_to: felt, amount_from: felt +) -> (amount_to: felt, r: felt) { + let (amm_from_balance, amm_to_balance, amount_to, r) = do_swap_lets(account_id, token_from, token_to, amount_from); + do_swap_from_balance(account_id, token_from, amount_from, amm_from_balance); + do_swap_to_balance(account_id, token_to, amount_to, amm_to_balance); + return (amount_to=amount_to, r=r); +} + +// @post (token_type == TOKEN_TYPE_A and $Return.t == TOKEN_TYPE_B) or (token_type != TOKEN_TYPE_A and $Return.t == TOKEN_TYPE_A) +func get_opposite_token(token_type: felt) -> (t: felt) { + if (token_type == TOKEN_TYPE_A) { + return (TOKEN_TYPE_B,); + } else { + return (TOKEN_TYPE_A,); + } +} + +// Adds demo tokens to the given account. +// @storage_update account_balance(account_id, TOKEN_TYPE_A) := account_balance(account_id, TOKEN_TYPE_A) + token_a_amount +// @storage_update account_balance(account_id, TOKEN_TYPE_B) := account_balance(account_id, TOKEN_TYPE_B) + token_b_amount +func add_demo_token{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( + account_id: felt, token_a_amount: felt, token_b_amount: felt +) { + // Make sure the account's balance is much smaller then pool init balance. + assert_nn_le(token_a_amount, ACCOUNT_BALANCE_BOUND - 1); + assert_nn_le(token_b_amount, ACCOUNT_BALANCE_BOUND - 1); + modify_account_balance(account_id=account_id, token_type=TOKEN_TYPE_A, amount=token_a_amount); + modify_account_balance(account_id=account_id, token_type=TOKEN_TYPE_B, amount=token_b_amount); + return (); +} + +// Until we have LPs, for testing, we'll need to initialize the AMM somehow. +// @storage_update pool_balance(TOKEN_TYPE_A) := token_a +// @storage_update pool_balance(TOKEN_TYPE_B) := token_b +func init_pool{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( + token_a: felt, token_b: felt +) { + assert_nn_le(token_a, POOL_UPPER_BOUND - 1); + assert_nn_le(token_b, POOL_UPPER_BOUND - 1); + set_pool_token_balance(token_type=TOKEN_TYPE_A, balance=token_a); + set_pool_token_balance(token_type=TOKEN_TYPE_B, balance=token_b); + return (); +} diff --git a/tests/resources/golden/toy_amm_split.gold b/tests/resources/golden/toy_amm_split.gold new file mode 100644 index 00000000..3867bf66 --- /dev/null +++ b/tests/resources/golden/toy_amm_split.gold @@ -0,0 +1,44 @@ +add_demo_token +Verified + +do_swap +Verified + +do_swap_from_balance +Verified + +do_swap_lets +Verified + +do_swap_to_balance +Verified + +get_account_token_balance +Verified + +get_opposite_token +Verified + +get_pool_token_balance +Verified + +init_pool +Verified + +modify_account_balance +Verified + +set_pool_token_balance +Verified + +math.assert_le +Verified + +math.assert_nn +Verified + +math.assert_nn_le +Verified + +math.unsigned_div_rem +Verified From 906b94f9b0296928fc8206ec2ae51128b0c9e80f Mon Sep 17 00:00:00 2001 From: Julian Sutherland Date: Sun, 5 Feb 2023 01:03:55 +0000 Subject: [PATCH 3/7] small lint --- src/Horus/Global.hs | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/src/Horus/Global.hs b/src/Horus/Global.hs index 127cc7e7..624e0e51 100644 --- a/src/Horus/Global.hs +++ b/src/Horus/Global.hs @@ -247,16 +247,16 @@ removeMathSAT m run = do let solver = cfg_solver conf usesLvars <- or <$> traverse instUsesLvars (m_prog m) if (includesMathsat solver && usesLvars) - then do - let solver' = filterMathsat solver - if isEmptySolver solver' - then throw "Only the MathSAT solver was used to analyze a call with a logical variable in its specification." - else do - setConfig conf{cfg_solver = solver'} - result <- run - setConfig conf - pure result - else run + then do + let solver' = filterMathsat solver + if isEmptySolver solver' + then throw "Only the MathSAT solver was used to analyze a call with a logical variable in its specification." + else do + setConfig conf{cfg_solver = solver'} + result <- run + setConfig conf + pure result + else run where -- FIXME should check not just pre, but also post instUsesLvars i = falseIfError $ do From d3881f2dc999797421afb24181c16ae963a8e528 Mon Sep 17 00:00:00 2001 From: Julian Sutherland Date: Sun, 5 Feb 2023 01:21:04 +0000 Subject: [PATCH 4/7] lint fix plus removed toy_amm_split test as MathSAT does not run in CI --- src/Horus/Global.hs | 2 +- .../golden/{ => toy_amm}/toy_amm_split.cairo | 0 .../golden/{ => toy_amm}/toy_amm_split.gold | 0 ..._amm_with_split_and_original_do_swap.cairo | 257 ------------------ 4 files changed, 1 insertion(+), 258 deletions(-) rename tests/resources/golden/{ => toy_amm}/toy_amm_split.cairo (100%) rename tests/resources/golden/{ => toy_amm}/toy_amm_split.gold (100%) delete mode 100644 tests/resources/golden/toy_amm/toy_amm_with_split_and_original_do_swap.cairo diff --git a/src/Horus/Global.hs b/src/Horus/Global.hs index 624e0e51..3c72d9a5 100644 --- a/src/Horus/Global.hs +++ b/src/Horus/Global.hs @@ -246,7 +246,7 @@ removeMathSAT m run = do conf <- getConfig let solver = cfg_solver conf usesLvars <- or <$> traverse instUsesLvars (m_prog m) - if (includesMathsat solver && usesLvars) + if includesMathsat solver && usesLvars then do let solver' = filterMathsat solver if isEmptySolver solver' diff --git a/tests/resources/golden/toy_amm_split.cairo b/tests/resources/golden/toy_amm/toy_amm_split.cairo similarity index 100% rename from tests/resources/golden/toy_amm_split.cairo rename to tests/resources/golden/toy_amm/toy_amm_split.cairo diff --git a/tests/resources/golden/toy_amm_split.gold b/tests/resources/golden/toy_amm/toy_amm_split.gold similarity index 100% rename from tests/resources/golden/toy_amm_split.gold rename to tests/resources/golden/toy_amm/toy_amm_split.gold diff --git a/tests/resources/golden/toy_amm/toy_amm_with_split_and_original_do_swap.cairo b/tests/resources/golden/toy_amm/toy_amm_with_split_and_original_do_swap.cairo deleted file mode 100644 index 7ea1f7b0..00000000 --- a/tests/resources/golden/toy_amm/toy_amm_with_split_and_original_do_swap.cairo +++ /dev/null @@ -1,257 +0,0 @@ -%lang starknet - -%builtins pedersen -from starkware.cairo.common.cairo_builtins import HashBuiltin - -from starkware.cairo.common.hash import hash2 - -from math import assert_le, assert_nn_le, unsigned_div_rem -// The maximum amount of each token that belongs to the AMM. - -const BALANCE_UPPER_BOUND = 2 ** 64; -const TOKEN_TYPE_A = 1; -const TOKEN_TYPE_B = 2; - -// Ensure the user's balances are much smaller than the pool's balance. - -const POOL_UPPER_BOUND = 2 ** 30; - -const ACCOUNT_BALANCE_BOUND = 1073741; // 2**30 // 1000. - -// A map from account and token type to the corresponding balance of that account. - -@storage_var - -func account_balance(account_id: felt, token_type: felt) -> (balance: felt) { - -} - -// A map from token type to the corresponding balance of the pool. - -@storage_var - -func pool_balance(token_type: felt) -> (balance: felt) { - -} - -// Adds amount to the account's balance for the given token. - -// amount may be positive or negative. - -// Assert before setting that the balance does not exceed the upper bound. - -// - -// @storage_update account_balance(account_id, token_type) := account_balance(account_id, token_type) + amount - -func modify_account_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( - - account_id: felt, token_type: felt, amount: felt - -) { - - let (current_balance) = account_balance.read(account_id, token_type); - - tempvar new_balance = current_balance + amount; - - assert_nn_le(new_balance, BALANCE_UPPER_BOUND - 1); - - account_balance.write(account_id=account_id, token_type=token_type, value=new_balance); - - return (); - -} - -// Returns the account's balance for the given token. - -// - -// @post $Return.balance == account_balance(account_id, token_type) - -func get_account_token_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( - - account_id: felt, token_type: felt - -) -> (balance: felt) { - - return account_balance.read(account_id, token_type); - -} - -// Sets the pool's balance for the given token. -// Asserts before setting that the balance does not exceed the upper bound. -// -// @storage_update pool_balance(token_type) := balance - -func set_pool_token_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( - - token_type: felt, balance: felt - -) { - - assert_nn_le(balance, BALANCE_UPPER_BOUND - 1); - - pool_balance.write(token_type, balance); - - return (); - -} - -// Returns the pool's balance. -// @post $Return.balance == pool_balance(token_type) -func get_pool_token_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( - - token_type: felt - -) -> (balance: felt) { - - return pool_balance.read(token_type); - -} - -// Swaps tokens between the given account and the pool. -// -// @declare $old_pool_balance_from: felt -// @declare $old_pool_balance_to: felt -// @pre pool_balance(token_from) == $old_pool_balance_from -// @pre pool_balance(token_to) == $old_pool_balance_to -// -// Tokens should be different -// @pre (token_from == TOKEN_TYPE_A and token_to == TOKEN_TYPE_B) -// -// The account has enough balance -// @pre 0 < amount_from and amount_from <= account_balance(account_id, token_from) -// -// The pool balances are positive -// @pre pool_balance(token_to) >= 0 -// @pre pool_balance(token_from) >= 0 -// -// Assumptions needed for unsigned_div_rem to not overflow -// @pre pool_balance(token_from) + amount_from <= 10633823966279326983230456482242756608 -// @pre pool_balance(token_to) * amount_from < 2**128 * (pool_balance(token_from) + amount_from) -// -// The returned amount_to is correct. -// @post $Return.amm_from_balance == pool_balance(token_from) -// @post $Return.amm_to_balance == pool_balance(token_to) -// @post $old_pool_balance_to * amount_from == $Return.amount_to * ($old_pool_balance_from + amount_from) + $Return.r -// The pool balances are positive -// @post $Return.amm_to_balance >= 0 -// @post $Return.amm_from_balance >= 0 -func do_swap_lets{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( - account_id: felt, token_from: felt, token_to: felt, amount_from: felt -) -> (amm_from_balance: felt, amm_to_balance: felt, amount_to: felt, r: felt) { - alloc_locals; - // Get pool balance. - let (local amm_from_balance) = get_pool_token_balance(token_type=token_from); - let (local amm_to_balance) = get_pool_token_balance(token_type=token_to); - // Calculate swap amount. - let (local amount_to, local r) = unsigned_div_rem( - amm_to_balance * amount_from, amm_from_balance + amount_from - ); - return (amm_from_balance=amm_from_balance, amm_to_balance=amm_to_balance, amount_to=amount_to, r=r); -} -// Swaps tokens between the given account and the pool. -// -// Pool balance is updated -// @storage_update pool_balance(token_from) := amm_from_balance + amount_from -// -// Account balance is updated -// @storage_update account_balance(account_id, token_from) := account_balance(account_id, token_from) - amount_from -func do_swap_from_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( - account_id: felt, token_from: felt, amount_from: felt, amm_from_balance: felt, -) -> () { - // Update token_from balances. - modify_account_balance(account_id=account_id, token_type=token_from, amount=-amount_from); - set_pool_token_balance(token_type=token_from, balance=amm_from_balance + amount_from); - return (); - -} -// Swaps tokens between the given account and the pool. -// -// Pool balance is updated -// @storage_update pool_balance(token_to) := amm_to_balance - amount_to -// -// Account balance is updated -// @storage_update account_balance(account_id, token_to) := account_balance(account_id, token_to) + amount_to -func do_swap_to_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( - account_id: felt, token_to: felt, amount_to: felt, amm_to_balance: felt, -) -> () { - // Update token_to balances. - modify_account_balance(account_id=account_id, token_type=token_to, amount=amount_to); - set_pool_token_balance(token_type=token_to, balance=amm_to_balance - amount_to); - return (); -} - -// Swaps tokens between the given account and the pool. -// -// @declare $old_pool_balance_from: felt -// @declare $old_pool_balance_to: felt -// @pre pool_balance(token_from) == $old_pool_balance_from -// @pre pool_balance(token_to) == $old_pool_balance_to -// -// Tokens should be different -// @pre (token_from == TOKEN_TYPE_A and token_to == TOKEN_TYPE_B) -// -// The account has enough balance -// @pre 0 < amount_from and amount_from <= account_balance(account_id, token_from) -// -// The pool balances are positive -// @pre pool_balance(token_to) >= 0 -// @pre pool_balance(token_from) >= 0 -// -// Assumptions needed for unsigned_div_rem to not overflow -// @pre pool_balance(token_from) + amount_from <= 10633823966279326983230456482242756608 -// @pre pool_balance(token_to) * amount_from < 2**128 * (pool_balance(token_from) + amount_from) -// -// Pool balance is updated -// @storage_update pool_balance(token_from) := pool_balance(token_from) + amount_from -// @storage_update pool_balance(token_to) := pool_balance(token_to) - $Return.amount_to -// -// Account balance is updated -// @storage_update account_balance(account_id, token_from) := account_balance(account_id, token_from) - amount_from -// @storage_update account_balance(account_id, token_to) := account_balance(account_id, token_to) + $Return.amount_to -// -// The returned amount_to is correct. -// @post $old_pool_balance_to * amount_from == $Return.amount_to * ($old_pool_balance_from + amount_from) + $Return.r -func do_swap{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( - account_id: felt, token_from: felt, token_to: felt, amount_from: felt -) -> (amount_to: felt, r: felt) { - let (amm_from_balance, amm_to_balance, amount_to, r) = do_swap_lets(account_id, token_from, token_to, amount_from); - do_swap_from_balance(account_id, token_from, amount_from, amm_from_balance); - do_swap_to_balance(account_id, token_to, amount_to, amm_to_balance); - return (amount_to=amount_to, r=r); -} - -// @post (token_type == TOKEN_TYPE_A and $Return.t == TOKEN_TYPE_B) or (token_type != TOKEN_TYPE_A and $Return.t == TOKEN_TYPE_A) -func get_opposite_token(token_type: felt) -> (t: felt) { - if (token_type == TOKEN_TYPE_A) { - return (TOKEN_TYPE_B,); - } else { - return (TOKEN_TYPE_A,); - } -} -// Adds demo tokens to the given account. -// @storage_update account_balance(account_id, TOKEN_TYPE_A) := account_balance(account_id, TOKEN_TYPE_A) + token_a_amount -// @storage_update account_balance(account_id, TOKEN_TYPE_B) := account_balance(account_id, TOKEN_TYPE_B) + token_b_amount -func add_demo_token{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( - account_id: felt, token_a_amount: felt, token_b_amount: felt -) { - // Make sure the account's balance is much smaller then pool init balance. - assert_nn_le(token_a_amount, ACCOUNT_BALANCE_BOUND - 1); - assert_nn_le(token_b_amount, ACCOUNT_BALANCE_BOUND - 1); - modify_account_balance(account_id=account_id, token_type=TOKEN_TYPE_A, amount=token_a_amount); - modify_account_balance(account_id=account_id, token_type=TOKEN_TYPE_B, amount=token_b_amount); - return (); -} -// Until we have LPs, for testing, we'll need to initialize the AMM somehow. -// @storage_update pool_balance(TOKEN_TYPE_A) := token_a -// @storage_update pool_balance(TOKEN_TYPE_B) := token_b -func init_pool{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( - token_a: felt, token_b: felt -) { - assert_nn_le(token_a, POOL_UPPER_BOUND - 1); - assert_nn_le(token_b, POOL_UPPER_BOUND - 1); - set_pool_token_balance(token_type=TOKEN_TYPE_A, balance=token_a); - set_pool_token_balance(token_type=TOKEN_TYPE_B, balance=token_b); - return (); -} \ No newline at end of file From 3d2f14cb7bedda0574066ab723295189a3610bc7 Mon Sep 17 00:00:00 2001 From: Julian Sutherland Date: Sun, 5 Feb 2023 01:28:06 +0000 Subject: [PATCH 5/7] Added disjunction to pre of toy amm example as it now works --- tests/resources/golden/toy_amm/toy_amm_split.cairo | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/resources/golden/toy_amm/toy_amm_split.cairo b/tests/resources/golden/toy_amm/toy_amm_split.cairo index c3960d6f..61d75c59 100644 --- a/tests/resources/golden/toy_amm/toy_amm_split.cairo +++ b/tests/resources/golden/toy_amm/toy_amm_split.cairo @@ -192,7 +192,7 @@ func do_swap_to_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_ch // @pre pool_balance(token_to) == $old_pool_balance_to // // Tokens should be different -// @pre (token_from == TOKEN_TYPE_A and token_to == TOKEN_TYPE_B) +// @pre (token_from == TOKEN_TYPE_A and token_to == TOKEN_TYPE_B) or (token_from == TOKEN_TYPE_B and token_to == TOKEN_TYPE_A) // // The account has enough balance // @pre 0 < amount_from and amount_from <= account_balance(account_id, token_from) From 9ae1fde9bcba21285abfe3d1a1816b1ba10e94de Mon Sep 17 00:00:00 2001 From: Julian Sutherland Date: Tue, 7 Feb 2023 13:00:32 +0000 Subject: [PATCH 6/7] removed extra file and fixes to pre of toy amm --- .../golden/toy_amm/split_toy_amm.cairo | 217 ------------------ .../golden/toy_amm/toy_amm_split.cairo | 2 +- 2 files changed, 1 insertion(+), 218 deletions(-) delete mode 100644 tests/resources/golden/toy_amm/split_toy_amm.cairo diff --git a/tests/resources/golden/toy_amm/split_toy_amm.cairo b/tests/resources/golden/toy_amm/split_toy_amm.cairo deleted file mode 100644 index 0c978a72..00000000 --- a/tests/resources/golden/toy_amm/split_toy_amm.cairo +++ /dev/null @@ -1,217 +0,0 @@ -%lang starknet - -%builtins pedersen -from starkware.cairo.common.cairo_builtins import HashBuiltin - -from starkware.cairo.common.hash import hash2 - -from math import assert_le, assert_nn_le, unsigned_div_rem -// The maximum amount of each token that belongs to the AMM. - -const BALANCE_UPPER_BOUND = 2 ** 64; -const TOKEN_TYPE_A = 1; -const TOKEN_TYPE_B = 2; - -// Ensure the user's balances are much smaller than the pool's balance. - -const POOL_UPPER_BOUND = 2 ** 30; - -const ACCOUNT_BALANCE_BOUND = 1073741; // 2**30 // 1000. - -// A map from account and token type to the corresponding balance of that account. - -@storage_var - -func account_balance(account_id: felt, token_type: felt) -> (balance: felt) { - -} - -// A map from token type to the corresponding balance of the pool. - -@storage_var - -func pool_balance(token_type: felt) -> (balance: felt) { - -} - -// Adds amount to the account's balance for the given token. - -// amount may be positive or negative. - -// Assert before setting that the balance does not exceed the upper bound. - -// - -// @storage_update account_balance(account_id, token_type) := account_balance(account_id, token_type) + amount - -func modify_account_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( - - account_id: felt, token_type: felt, amount: felt - -) { - - let (current_balance) = account_balance.read(account_id, token_type); - - tempvar new_balance = current_balance + amount; - - assert_nn_le(new_balance, BALANCE_UPPER_BOUND - 1); - - account_balance.write(account_id=account_id, token_type=token_type, value=new_balance); - - return (); - -} - -// Returns the account's balance for the given token. - -// - -// @post $Return.balance == account_balance(account_id, token_type) - -func get_account_token_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( - - account_id: felt, token_type: felt - -) -> (balance: felt) { - - return account_balance.read(account_id, token_type); - -} - -// Sets the pool's balance for the given token. -// Asserts before setting that the balance does not exceed the upper bound. -// -// @storage_update pool_balance(token_type) := balance - -func set_pool_token_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( - - token_type: felt, balance: felt - -) { - - assert_nn_le(balance, BALANCE_UPPER_BOUND - 1); - - pool_balance.write(token_type, balance); - - return (); - -} - -// Returns the pool's balance. -// @post $Return.balance == pool_balance(token_type) -func get_pool_token_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( - - token_type: felt - -) -> (balance: felt) { - - return pool_balance.read(token_type); - -} - -// Swaps tokens between the given account and the pool. -// -// @declare $old_pool_balance_from: felt -// @declare $old_pool_balance_to: felt -// @pre pool_balance(token_from) == $old_pool_balance_from -// @pre pool_balance(token_to) == $old_pool_balance_to -// -// Tokens should be different -// @pre (token_from == TOKEN_TYPE_A and token_to == TOKEN_TYPE_B) -// -// The account has enough balance -// @pre 0 < amount_from and amount_from <= account_balance(account_id, token_from) -// -// The pool balances are positive -// @pre pool_balance(token_to) >= 0 -// @pre pool_balance(token_from) >= 0 -// -// Assumptions needed for unsigned_div_rem to not overflow -// @pre pool_balance(token_from) + amount_from <= 10633823966279326983230456482242756608 -// @pre pool_balance(token_to) * amount_from < 2**128 * (pool_balance(token_from) + amount_from) -// -// The returned amount_to is correct. -// @post $Return.amm_from_balance == pool_balance(token_from) -// @post $Return.amm_to_balance == pool_balance(token_to) -// @post $old_pool_balance_to * amount_from == $Return.amount_to * ($old_pool_balance_from + amount_from) + $Return.r -// The pool balances are positive -// @post $Return.amm_to_balance >= 0 -// @post $Return.amm_from_balance >= 0 -func do_swap_lets{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( - account_id: felt, token_from: felt, token_to: felt, amount_from: felt -) -> (amm_from_balance: felt, amm_to_balance: felt, amount_to: felt, r: felt) { - alloc_locals; - // Get pool balance. - let (local amm_from_balance) = get_pool_token_balance(token_type=token_from); - let (local amm_to_balance) = get_pool_token_balance(token_type=token_to); - // Calculate swap amount. - let (local amount_to, local r) = unsigned_div_rem( - amm_to_balance * amount_from, amm_from_balance + amount_from - ); - return (amm_from_balance=amm_from_balance, amm_to_balance=amm_to_balance, amount_to=amount_to, r=r); -} -// Swaps tokens between the given account and the pool. -// -// Pool balance is updated -// @storage_update pool_balance(token_from) := amm_from_balance + amount_from -// -// Account balance is updated -// @storage_update account_balance(account_id, token_from) := account_balance(account_id, token_from) - amount_from -func do_swap_from_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( - account_id: felt, token_from: felt, amount_from: felt, amm_from_balance: felt, -) -> () { - // Update token_from balances. - modify_account_balance(account_id=account_id, token_type=token_from, amount=-amount_from); - set_pool_token_balance(token_type=token_from, balance=amm_from_balance + amount_from); - return (); - -} -// Swaps tokens between the given account and the pool. -// -// Pool balance is updated -// @storage_update pool_balance(token_to) := amm_to_balance - amount_to -// -// Account balance is updated -// @storage_update account_balance(account_id, token_to) := account_balance(account_id, token_to) + amount_to -func do_swap_to_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( - account_id: felt, token_to: felt, amount_to: felt, amm_to_balance: felt, -) -> () { - // Update token_to balances. - modify_account_balance(account_id=account_id, token_type=token_to, amount=amount_to); - set_pool_token_balance(token_type=token_to, balance=amm_to_balance - amount_to); - return (); -} - -// @post (token_type == TOKEN_TYPE_A and $Return.t == TOKEN_TYPE_B) or (token_type != TOKEN_TYPE_A and $Return.t == TOKEN_TYPE_A) -func get_opposite_token(token_type: felt) -> (t: felt) { - if (token_type == TOKEN_TYPE_A) { - return (TOKEN_TYPE_B,); - } else { - return (TOKEN_TYPE_A,); - } -} -// Adds demo tokens to the given account. -// @storage_update account_balance(account_id, TOKEN_TYPE_A) := account_balance(account_id, TOKEN_TYPE_A) + token_a_amount -// @storage_update account_balance(account_id, TOKEN_TYPE_B) := account_balance(account_id, TOKEN_TYPE_B) + token_b_amount -func add_demo_token{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( - account_id: felt, token_a_amount: felt, token_b_amount: felt -) { - // Make sure the account's balance is much smaller then pool init balance. - assert_nn_le(token_a_amount, ACCOUNT_BALANCE_BOUND - 1); - assert_nn_le(token_b_amount, ACCOUNT_BALANCE_BOUND - 1); - modify_account_balance(account_id=account_id, token_type=TOKEN_TYPE_A, amount=token_a_amount); - modify_account_balance(account_id=account_id, token_type=TOKEN_TYPE_B, amount=token_b_amount); - return (); -} -// Until we have LPs, for testing, we'll need to initialize the AMM somehow. -// @storage_update pool_balance(TOKEN_TYPE_A) := token_a -// @storage_update pool_balance(TOKEN_TYPE_B) := token_b -func init_pool{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( - token_a: felt, token_b: felt -) { - assert_nn_le(token_a, POOL_UPPER_BOUND - 1); - assert_nn_le(token_b, POOL_UPPER_BOUND - 1); - set_pool_token_balance(token_type=TOKEN_TYPE_A, balance=token_a); - set_pool_token_balance(token_type=TOKEN_TYPE_B, balance=token_b); - return (); -} \ No newline at end of file diff --git a/tests/resources/golden/toy_amm/toy_amm_split.cairo b/tests/resources/golden/toy_amm/toy_amm_split.cairo index 61d75c59..e332d7ea 100644 --- a/tests/resources/golden/toy_amm/toy_amm_split.cairo +++ b/tests/resources/golden/toy_amm/toy_amm_split.cairo @@ -117,7 +117,7 @@ func get_pool_token_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, rang // @pre pool_balance(token_to) == $old_pool_balance_to // // Tokens should be different -// @pre (token_from == TOKEN_TYPE_A and token_to == TOKEN_TYPE_B) +// @pre (token_from == TOKEN_TYPE_A and token_to == TOKEN_TYPE_B) or (token_from == TOKEN_TYPE_B and token_to == TOKEN_TYPE_A) // // The account has enough balance // @pre 0 < amount_from and amount_from <= account_balance(account_id, token_from) From f2374aaa0cfd37e56d03678c281965ddc3c5d37f Mon Sep 17 00:00:00 2001 From: Julian Sutherland Date: Tue, 7 Feb 2023 14:20:42 +0000 Subject: [PATCH 7/7] removed extra whitespace --- .../golden/toy_amm/toy_amm_split.cairo | 35 ------------------- 1 file changed, 35 deletions(-) diff --git a/tests/resources/golden/toy_amm/toy_amm_split.cairo b/tests/resources/golden/toy_amm/toy_amm_split.cairo index e332d7ea..93a16d60 100644 --- a/tests/resources/golden/toy_amm/toy_amm_split.cairo +++ b/tests/resources/golden/toy_amm/toy_amm_split.cairo @@ -13,37 +13,24 @@ const TOKEN_TYPE_A = 1; const TOKEN_TYPE_B = 2; // Ensure the user's balances are much smaller than the pool's balance. - const POOL_UPPER_BOUND = 2 ** 30; - const ACCOUNT_BALANCE_BOUND = 1073741; // 2**30 // 1000. // A map from account and token type to the corresponding balance of that account. - @storage_var - func account_balance(account_id: felt, token_type: felt) -> (balance: felt) { - } // A map from token type to the corresponding balance of the pool. - @storage_var - func pool_balance(token_type: felt) -> (balance: felt) { - } // Adds amount to the account's balance for the given token. - // amount may be positive or negative. - // Assert before setting that the balance does not exceed the upper bound. - // - // @storage_update account_balance(account_id, token_type) := account_balance(account_id, token_type) + amount - func modify_account_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( account_id: felt, token_type: felt, amount: felt @@ -51,62 +38,40 @@ func modify_account_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, rang ) { let (current_balance) = account_balance.read(account_id, token_type); - tempvar new_balance = current_balance + amount; - assert_nn_le(new_balance, BALANCE_UPPER_BOUND - 1); - account_balance.write(account_id=account_id, token_type=token_type, value=new_balance); - return (); - } // Returns the account's balance for the given token. - // - // @post $Return.balance == account_balance(account_id, token_type) - func get_account_token_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( - account_id: felt, token_type: felt - ) -> (balance: felt) { - return account_balance.read(account_id, token_type); - } // Sets the pool's balance for the given token. // Asserts before setting that the balance does not exceed the upper bound. // // @storage_update pool_balance(token_type) := balance - func set_pool_token_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( - token_type: felt, balance: felt ) { - assert_nn_le(balance, BALANCE_UPPER_BOUND - 1); - pool_balance.write(token_type, balance); - return (); - } // Returns the pool's balance. // @post $Return.balance == pool_balance(token_type) func get_pool_token_balance{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}( - token_type: felt - ) -> (balance: felt) { - return pool_balance.read(token_type); - } // Swaps tokens between the given account and the pool.