Merge branch 'master' into _update-deps/runtimeverification/blockchai…

…n-k-plugin

Makefile

@@ -6,6 +6,7 @@
         test unittest-python mandos-test test-elrond-contracts                   \
         test-elrond-adder test-elrond-crowdfunding-esdt                          \
         test-elrond-multisig test-elrond-basic-features                          \
+				test-elrond-alloc-features                                               \
         test-elrond-addercaller test-elrond-callercallee test-custom-contracts   \
         rule-coverage clean-coverage                                             \
 
@@ -259,7 +260,8 @@ KRUN_OPTS :=
 elrond-contract-deps := test-elrond-adder             \
                         test-elrond-crowdfunding-esdt \
                         test-elrond-multisig          \
-                        test-elrond-basic-features
+                        test-elrond-basic-features    \
+												test-elrond-alloc-features
 test-elrond-contracts: $(elrond-contract-deps)
 
 test: test-simple mandos-test test-elrond-contracts test-custom-contracts
@@ -354,6 +356,9 @@ test-elrond-basic-features: $(elrond_basic_features_tests:=.mandos)
 $(ELROND_BASIC_FEATURES_DIR)/scenarios/%.scen.json.mandos: $(llvm_kompiled) $(ELROND_BASIC_FEATURES_WASM) poetry-install
 	$(TEST_MANDOS) $(ELROND_BASIC_FEATURES_DIR)/scenarios/$*.scen.json --log-level none
 
+tests/custom-scenarios/basic-features/%.scen.json.mandos: $(llvm_kompiled) $(ELROND_BASIC_FEATURES_WASM) poetry-install
+	$(TEST_MANDOS) tests/custom-scenarios/basic-features/$*.scen.json --log-level none
+
 ## Alloc Features Test
 
 ELROND_ALLOC_FEATURES_DIR=$(ELROND_CONTRACT)/feature-tests/alloc-features

esdt.md

@@ -126,7 +126,45 @@ module ESDT
         <commands> esdtLocalMint(ADDR, TOK, VAL)
                 => addToESDTBalance(ADDR, TOK, VAL) ...
         </commands>
-        <vmOutput> _ => VMOutput(OK, b"", .ListBytes, .List)</vmOutput>
+```
+
+### Local Burn
+
+```k
+    syntax BuiltinFunction ::= "#ESDTLocalBurn"        [klabel(#ESDTLocalBurn), symbol]
+    rule toBuiltinFunction(F) => #ESDTLocalBurn requires F ==K #token("\"ESDTLocalBurn\"", "WasmStringToken")
+
+    rule [ESDTLocalBurn]:
+        <commands> processBuiltinFunction(#ESDTLocalBurn, SND, DST, <vmInput> 
+                                                                    <callValue> VALUE </callValue>
+                                                                    <callArgs> ARGS </callArgs>
+                                                                    _ 
+                                                                  </vmInput>)
+                => checkBool(VALUE ==Int 0, "built in function called with tx value is not allowed")
+                ~> checkBool(size(ARGS) >=Int 2, "invalid arguments to process built-in function")
+                ~> checkBool(SND ==K DST, "invalid receiver address")
+                ~> checkAccountExists(SND)
+                // TODO If the token has the 'BurnRoleForAll' global property, skip 'checkAllowedToExecute'
+                ~> checkAllowedToExecute(SND, ARGS {{ 0 }} orDefault b"", ESDTRoleLocalBurn) 
+                ~> checkBool( lengthBytes(ARGS {{ 1 }} orDefault b"") <=Int 100
+                            , "invalid arguments to process built-in function")
+                ~> esdtLocalBurn( SND
+                                , ARGS {{ 0 }} orDefault b""
+                                , Bytes2Int(ARGS {{ 1 }} orDefault b"", BE, Unsigned)
+                                )
+                   ...
+        </commands>
+
+    syntax InternalCmd ::= esdtLocalBurn(account: Bytes, token: Bytes, value: Int)
+        [klabel(esdtLocalBurn), symbol]
+ // ------------------------------------------------------------------------------
+    rule [esdtLocalBurn-cmd]:
+        <commands> esdtLocalBurn(ADDR, TOK, VAL)
+                => checkESDTBalance(ADDR, TOK, VAL)
+                ~> addToESDTBalance(ADDR, TOK, 0 -Int VAL)
+                   ...
+        </commands>
+
 ```
 
 ### ESDT Transfer
@@ -186,7 +224,6 @@ module ESDT
         <commands> determineIsSCCallAfter(_SND, _DST, _FUNC, _VMINPUT)
                 => . ...
         </commands>
-        <vmOutput> _ => VMOutput(OK, b"", .ListBytes, .List)</vmOutput> // TODO add log entry
       [owise]
 
     syntax VmInputCell ::= mkVmInputEsdtExec(Bytes, BuiltinFunction, ListBytes, Int, Int)

kmultiversx/src/kmultiversx/scenario.py

@@ -380,9 +380,17 @@ def mandos_to_check_account(address: str, sections: dict, filename: str) -> list
         k_steps.append(KApply('checkAccountCode', [address_value, k_code_path]))
     if ('esdt' in sections) and (sections['esdt'] != '*'):
         for token, value in sections['esdt'].items():
-            token_bytes = mandos_argument_to_kbytes(token)
-            value_kint = mandos_int_to_kint(value)
-            k_steps.append(KApply('checkAccountESDTBalance', [address_value, token_bytes, value_kint]))
+            token_kbytes = mandos_argument_to_kbytes(token)
+
+            value_kint = mandos_to_esdt_value(value)
+            if value_kint is not None:
+                step = KApply('checkAccountESDTBalance', [address_value, token_kbytes, value_kint])
+                k_steps.append(step)
+
+            roles = mandos_to_esdt_roles(value)
+            if roles is not None:
+                step = KApply('checkEsdtRoles', [address_value, token_kbytes, set_of(roles)])
+                k_steps.append(step)
 
     k_steps.append(KApply('checkedAccount', [address_value]))
     return k_steps

mandos.md

@@ -193,6 +193,23 @@ Only take the next step once both the Elrond node and Wasm are done executing.
         <commands> . </commands>
       [priority(61)]
 
+    syntax Step ::= checkEsdtRoles( Bytes , Bytes , Set )
+        [klabel(checkEsdtRoles), symbol]
+ // ----------------------------------------------------------------------------
+    rule [checkEsdtRoles]:
+        <k> checkEsdtRoles(ADDR, TOK, ROLES) => . ... </k>
+        <account>
+          <address> ADDR </address>
+          <esdtData>
+            <esdtId> TOK </esdtId>
+            <esdtRoles> ROLES </esdtRoles>
+            ...
+           </esdtData>
+          ...
+        </account>
+        <commands> . </commands>
+      [priority(60)]
+
     syntax Step ::= newAddress    ( Address, Int, Address ) [klabel(newAddress), symbol]
                   | newAddressAux ( Bytes, Int, Bytes )     [klabel(newAddressAux), symbol]
  // ---------------------------------------------------------------------------------------

tests/basic_features.test

@@ -73,3 +73,4 @@ deps/mx-sdk-rs/contracts/feature-tests/basic-features/scenarios/storage_u64.scen
 deps/mx-sdk-rs/contracts/feature-tests/basic-features/scenarios/storage_usize_bad.scen.json
 deps/mx-sdk-rs/contracts/feature-tests/basic-features/scenarios/storage_usize.scen.json
 deps/mx-sdk-rs/contracts/feature-tests/basic-features/scenarios/struct_eq.scen.json
+tests/custom-scenarios/basic-features/storage_mapper_fungible_token.scen.json

tests/contracts/test_pair/src/test_pair.rs

@@ -62,7 +62,7 @@ mod pair_proxy {
 }
 
 #[multiversx_sc::contract]
-pub trait TestMultisigContract {
+pub trait TestPairContract {
     #[storage_mapper("firstToken")]
     fn first_token(&self) -> SingleValueMapper<TokenIdentifier>;
     #[storage_mapper("secondToken")]
@@ -140,6 +140,58 @@ pub trait TestMultisigContract {
         testapi::assume(BigUint::from(1000u32) < second_liquidity);
         testapi::assume(first_liquidity < max_liquidity);
         testapi::assume(second_liquidity < max_liquidity);
+
+        testapi::assume(BigUint::from(2u32) < first_value);
+        let first_no_percent = first_value.clone() * (MAX_PERCENTAGE - TOTAL_FEE_PERCENT);
+        testapi::assume((first_liquidity.clone() * MAX_PERCENTAGE + first_no_percent.clone()) < second_liquidity.clone() * first_no_percent );
+
+        testapi::set_esdt_balance(&liquidity_adder, &self.first_token().get(), &first_liquidity);
+        testapi::set_esdt_balance(&liquidity_adder, &self.second_token().get(), &second_liquidity);
+        testapi::set_esdt_balance(&alice, &self.first_token().get(), &first_value);
+
+        self.add_liquidity(
+            &pair, &liquidity_adder,
+            &first_liquidity, &second_liquidity,
+            &first_liquidity, &second_liquidity,
+        );
+
+        let first_reserve_initial = self.get_reserve(&pair, &self.first_token().get());
+        let second_reserve_initial = self.get_reserve(&pair, &self.second_token().get());
+
+        self.swap_tokens_fixed_input_first(
+            &pair, &alice, &first_value, &BigUint::from(1u64)
+        );
+
+        let first_reserve_final = self.get_reserve(&pair, &self.first_token().get());
+        let second_reserve_final = self.get_reserve(&pair, &self.second_token().get());
+
+        let total_fee = first_value.clone() * TOTAL_FEE_PERCENT / MAX_PERCENTAGE;
+        let special_fee = BigUint::zero();  // Fee not enabled
+                                            // first_value * SPECIAL_FEE_PERCENT / MAX_PERCENTAGE;
+        let initial_k = first_reserve_initial.clone() * second_reserve_initial.clone();
+        let final_k = first_reserve_final.clone() * second_reserve_final.clone();
+
+        require!(initial_k.clone() <= final_k.clone(), "K decreased!");
+        let condition = final_k <= initial_k.clone() + first_reserve_final.clone() + (total_fee.clone() - special_fee.clone() + 1u64) * second_reserve_final.clone();
+        require!(condition, "K grew too much!");
+        testapi::assert(initial_k.clone() <= final_k.clone());
+        // testapi::assert(final_k <= initial_k + first_reserve_initial + second_reserve_initial);
+    }
+
+    #[endpoint(test_add_liquidity)]
+    fn test_add_liquidity(&self, first_liquidity: BigUint, second_liquidity: BigUint, first_value: BigUint) {
+        let pair = ManagedAddress::from(PAIR);
+        let alice = ManagedAddress::from(ALICE);
+        let liquidity_adder = ManagedAddress::from(BOB);
+
+        let max_liquidity = self.get_max_mint_value() + 1000u32;
+
+        // make assumptions
+        testapi::assume(BigUint::from(1000u32) < first_liquidity);
+        testapi::assume(BigUint::from(1000u32) < second_liquidity);
+        testapi::assume(first_liquidity < max_liquidity);
+        testapi::assume(second_liquidity < max_liquidity);
+
         testapi::assume(BigUint::from(2u32) < first_value);
         let first_no_percent = first_value.clone() * (MAX_PERCENTAGE - TOTAL_FEE_PERCENT);
         testapi::assume((first_liquidity.clone() * MAX_PERCENTAGE + first_no_percent.clone()) < second_liquidity.clone() * first_no_percent );
@@ -154,6 +206,47 @@ pub trait TestMultisigContract {
             &first_liquidity, &second_liquidity,
         );
 
+        let lp_tokens = self.blockchain().get_esdt_balance(&liquidity_adder, &self.lp_token().get(), 0);
+        let first_reserve_initial = self.get_reserve(&pair, &self.first_token().get());
+        let second_reserve_initial = self.get_reserve(&pair, &self.second_token().get());
+
+        testapi::assert(first_liquidity == first_reserve_initial);
+        testapi::assert(second_liquidity == second_reserve_initial);
+        if first_liquidity < second_liquidity {
+          testapi::assert(lp_tokens == first_reserve_initial - 1000u64);
+        } else {
+          testapi::assert(lp_tokens == second_reserve_initial - 1000u64);
+        }
+    }
+
+    #[endpoint(test_swap)]
+    fn test_swap(&self, first_liquidity: BigUint, second_liquidity: BigUint, first_value: BigUint) {
+        let pair = ManagedAddress::from(PAIR);
+        let alice = ManagedAddress::from(ALICE);
+
+        let max_liquidity = self.get_max_mint_value() + 1000u32;
+
+        // make assumptions
+        testapi::assume(BigUint::from(1000u32) < first_liquidity);
+        testapi::assume(BigUint::from(1000u32) < second_liquidity);
+        testapi::assume(first_liquidity < second_liquidity);
+        testapi::assume(first_liquidity < max_liquidity);
+        testapi::assume(second_liquidity < max_liquidity);
+
+        testapi::assume(BigUint::from(2u32) < first_value);
+        let first_no_percent = first_value.clone() * (MAX_PERCENTAGE - TOTAL_FEE_PERCENT);
+        testapi::assume((first_liquidity.clone() * MAX_PERCENTAGE + first_no_percent.clone()) < second_liquidity.clone() * first_no_percent );
+
+        testapi::set_esdt_balance(&pair, &self.first_token().get(), &first_liquidity);
+        testapi::set_esdt_balance(&pair, &self.second_token().get(), &second_liquidity);
+        testapi::set_esdt_balance(&alice, &self.first_token().get(), &first_value);
+
+        let first_liquidity_bytes = first_liquidity.to_bytes_be_buffer();
+        let second_liquidity_bytes = second_liquidity.to_bytes_be_buffer();
+        testapi::set_storage(&pair, &ManagedBuffer::new_from_bytes(b"lp_token_supply"), &first_liquidity_bytes);
+        testapi::set_storage(&pair, &ManagedBuffer::new_from_bytes(b"reserve\x00\x00\x00\x0CFIRST-123456"), &first_liquidity_bytes);
+        testapi::set_storage(&pair, &ManagedBuffer::new_from_bytes(b"reserve\x00\x00\x00\x0DSECOND-123456"), &second_liquidity_bytes);
+
         let first_reserve_initial = self.get_reserve(&pair, &self.first_token().get());
         let second_reserve_initial = self.get_reserve(&pair, &self.second_token().get());
 
@@ -173,7 +266,7 @@ pub trait TestMultisigContract {
         require!(initial_k.clone() <= final_k.clone(), "K decreased!");
         let condition = final_k <= initial_k.clone() + first_reserve_final.clone() + (total_fee.clone() - special_fee.clone() + 1u64) * second_reserve_final.clone();
         require!(condition, "K grew too much!");
-        // testapi::assert(initial_k.clone() <= final_k.clone());
+        testapi::assert(initial_k.clone() <= final_k.clone());
         // testapi::assert(final_k <= initial_k + first_reserve_initial + second_reserve_initial);
     }
 
@@ -255,8 +348,11 @@ pub trait TestMultisigContract {
         testapi::stop_prank();
     }
 
+    // the ESDTLocalMint function limits its input to 100 bytes, which means
+    // that a contract can mint at most 2^(8*100) tokens.
     fn get_max_mint_value(&self) -> BigUint {
         // 800 = 11 0010 000
+        // 800 = 2^5 + 2^8 + 2^9
         // 2^800 = 2^512 * 2^256 * 2^32
         let a32 = BigUint::from(4294967296u64);
         let a64 = a32.clone() * a32.clone();

tests/contracts/test_pair/wasm/src/lib.rs

@@ -5,9 +5,9 @@
 ////////////////////////////////////////////////////
 
 // Init:                                 1
-// Endpoints:                            1
+// Endpoints:                            3
 // Async Callback (empty):               1
-// Total number of exported functions:   3
+// Total number of exported functions:   5
 
 #![no_std]
 #![feature(lang_items)]
@@ -20,6 +20,8 @@ multiversx_sc_wasm_adapter::endpoints! {
     (
         init => init
         test_exchange_k => test_exchange_k
+        test_add_liquidity => test_add_liquidity
+        test_swap => test_swap
     )
 }