Feature: symbolic execution support

Cargo.toml

@@ -182,4 +182,17 @@ members = [
   "contracts/feature-tests/scenario-tester/meta",
   "contracts/feature-tests/use-module",
   "contracts/feature-tests/use-module/meta",
+
+  "contracts/parametric-tests/adder-pt",
+  "contracts/parametric-tests/adder-pt/meta",
+  "contracts/parametric-tests/addercaller",
+  "contracts/parametric-tests/addercaller/meta",
+  "contracts/parametric-tests/callee",
+  "contracts/parametric-tests/callee/meta",
+  "contracts/parametric-tests/caller",
+  "contracts/parametric-tests/caller/meta",
+  "contracts/parametric-tests/multisig-pt",
+  "contracts/parametric-tests/multisig-pt/meta",
+  "contracts/parametric-tests/testapi-pt",
+  "contracts/parametric-tests/testapi-pt/meta",
 ]

contracts/examples/adder/sc-config.toml

@@ -2,3 +2,6 @@
 
 [[proxy]]
 path = "src/adder_proxy.rs"
+
+[[proxy]]
+path = "../../parametric-tests/adder-pt/src/adder_proxy.rs"

contracts/examples/multisig/sc-config.toml

@@ -17,3 +17,6 @@ add-labels = ["multisig-external-view"]
 
 [[proxy]]
 path = "src/multisig_proxy.rs"
+
+[[proxy]]
+path = "../../parametric-tests/multisig-pt/src/multisig_proxy.rs"

contracts/parametric-tests/adder-pt/.gitignore

@@ -0,0 +1,11 @@
+# Generated by Cargo
+# will have compiled files and executables
+/target/
+*/target/
+
+# The mxpy output
+/output*/
+
+# Kasmer
+.property
+generated_claims

contracts/parametric-tests/adder-pt/Cargo.toml

@@ -0,0 +1,21 @@
+[package]
+name = "adder-pt"
+version = "0.0.0"
+authors = [ "you",]
+edition = "2018"
+publish = false
+
+[lib]
+path = "src/adder_pt.rs"
+
+[dev-dependencies]
+num-bigint = "0.4.2"
+
+[dependencies.multiversx-sc]
+version = "0.50.0"
+path = "../../../framework/base"
+
+[dev-dependencies.multiversx-sc-scenario]
+version = "0.50.0"
+path = "../../../framework/scenario"
+

contracts/parametric-tests/adder-pt/README.md

@@ -0,0 +1,19 @@
+# Parametric test example for: Adder
+
+This is an example on how to write a basic parametric test contract.
+
+To run fuzzing on it using Kasmer, build the contracts and simply run
+
+```
+kasmer fuzz
+```
+
+
+To run symbolic execution:
+
+```
+kasmer build
+kasmer verify test_call_add --booster
+## and / or
+kasmer verify test_call_add_twice --booster
+```

contracts/parametric-tests/adder-pt/kasmer.json

@@ -0,0 +1,5 @@
+{
+  "contracts": [
+    "../../examples/adder"
+  ]
+}

contracts/parametric-tests/adder-pt/meta/Cargo.toml

@@ -0,0 +1,15 @@
+[package]
+name = "adder-pt-meta"
+version = "0.0.0"
+edition = "2018"
+publish = false
+authors = [ "you",]
+
+[dev-dependencies]
+
+[dependencies.adder-pt]
+path = ".."
+
+[dependencies.multiversx-sc-meta]
+version = "0.50.0"
+path = "../../../../framework/meta"

contracts/parametric-tests/adder-pt/meta/src/main.rs

@@ -0,0 +1,3 @@
+fn main() {
+    multiversx_sc_meta::cli_main::<adder_pt::AbiProvider>();
+}

contracts/parametric-tests/adder-pt/multiversx.json

@@ -0,0 +1,3 @@
+{
+    "language": "rust"
+}

contracts/parametric-tests/adder-pt/scenarios/test-adder.scen.json

@@ -0,0 +1,71 @@
+{
+    "name": "test-adder",
+    "comment": "run foundry-like test for Adder",
+    "gasSchedule": "v3",
+    "steps": [
+        {
+            "step": "setState",
+            "accounts": {
+                "address:k": {
+                    "nonce": "1",
+                    "balance": "100000"
+                }
+            },
+            "newAddresses": [
+                {
+                    "creatorAddress": "address:k",
+                    "creatorNonce": "1",
+                    "newAddress": "sc:k-test"
+                }
+            ]
+        },
+        {
+            "step": "fetchWasmSource",
+            "wasmPath": "file:../../../../deps/mx-sdk-rs/contracts/examples/adder/output/adder.wasm" 
+        },
+        {
+            "step": "scDeploy",
+            "id": "deploy test",
+            "comment": "deploy the test contract",
+            "tx": {
+                "from": "address:k",
+                "contractCode": "file:../output/test-adder.wasm",
+                "arguments": [
+                    "file:../../../../deps/mx-sdk-rs/contracts/examples/adder/output/adder.wasm"
+                ],
+                "gasLimit": "5,000,000,000,000",
+                "gasPrice": "0"
+            },
+            "expect": {
+                "out": [],
+                "status": "",
+                "logs": "*",
+                "gas": "*",
+                "refund": "*"
+            }
+        },
+        {
+            "step": "scCall",
+            "id": "call test",
+            "comment": "call the parametric test endpoint with a concrete value",
+            "tx": {
+                "from": "address:k",
+                "to": "sc:k-test",
+                "function": "test_call_add",
+                "value": "0",
+                "arguments": [
+                    "3"
+                ],
+                "gasLimit": "5,000,000",
+                "gasPrice": "0"
+            },
+            "expect": {
+                "out": [],
+                "status": "",
+                "logs": "*",
+                "gas": "*",
+                "refund": "*"
+            }
+        }
+    ]
+}

contracts/parametric-tests/adder-pt/src/adder_proxy.rs

@@ -0,0 +1,114 @@
+// Code generated by the multiversx-sc proxy generator. DO NOT EDIT.
+
+////////////////////////////////////////////////////
+////////////////// AUTO-GENERATED //////////////////
+////////////////////////////////////////////////////
+
+#![allow(dead_code)]
+#![allow(clippy::all)]
+
+use multiversx_sc::proxy_imports::*;
+
+pub struct AdderProxy;
+
+impl<Env, From, To, Gas> TxProxyTrait<Env, From, To, Gas> for AdderProxy
+where
+    Env: TxEnv,
+    From: TxFrom<Env>,
+    To: TxTo<Env>,
+    Gas: TxGas<Env>,
+{
+    type TxProxyMethods = AdderProxyMethods<Env, From, To, Gas>;
+
+    fn proxy_methods(self, tx: Tx<Env, From, To, (), Gas, (), ()>) -> Self::TxProxyMethods {
+        AdderProxyMethods { wrapped_tx: tx }
+    }
+}
+
+pub struct AdderProxyMethods<Env, From, To, Gas>
+where
+    Env: TxEnv,
+    From: TxFrom<Env>,
+    To: TxTo<Env>,
+    Gas: TxGas<Env>,
+{
+    wrapped_tx: Tx<Env, From, To, (), Gas, (), ()>,
+}
+
+#[rustfmt::skip]
+impl<Env, From, Gas> AdderProxyMethods<Env, From, (), Gas>
+where
+    Env: TxEnv,
+    Env::Api: VMApi,
+    From: TxFrom<Env>,
+    Gas: TxGas<Env>,
+{
+    pub fn init<
+        Arg0: ProxyArg<BigUint<Env::Api>>,
+    >(
+        self,
+        initial_value: Arg0,
+    ) -> TxTypedDeploy<Env, From, NotPayable, Gas, ()> {
+        self.wrapped_tx
+            .payment(NotPayable)
+            .raw_deploy()
+            .argument(&initial_value)
+            .original_result()
+    }
+}
+
+#[rustfmt::skip]
+impl<Env, From, To, Gas> AdderProxyMethods<Env, From, To, Gas>
+where
+    Env: TxEnv,
+    Env::Api: VMApi,
+    From: TxFrom<Env>,
+    To: TxTo<Env>,
+    Gas: TxGas<Env>,
+{
+    pub fn upgrade<
+        Arg0: ProxyArg<BigUint<Env::Api>>,
+    >(
+        self,
+        initial_value: Arg0,
+    ) -> TxTypedUpgrade<Env, From, To, NotPayable, Gas, ()> {
+        self.wrapped_tx
+            .payment(NotPayable)
+            .raw_upgrade()
+            .argument(&initial_value)
+            .original_result()
+    }
+}
+
+#[rustfmt::skip]
+impl<Env, From, To, Gas> AdderProxyMethods<Env, From, To, Gas>
+where
+    Env: TxEnv,
+    Env::Api: VMApi,
+    From: TxFrom<Env>,
+    To: TxTo<Env>,
+    Gas: TxGas<Env>,
+{
+    pub fn sum(
+        self,
+    ) -> TxTypedCall<Env, From, To, NotPayable, Gas, BigUint<Env::Api>> {
+        self.wrapped_tx
+            .payment(NotPayable)
+            .raw_call("getSum")
+            .original_result()
+    }
+
+    /// Add desired amount to the storage variable. 
+    pub fn add<
+        Arg0: ProxyArg<BigUint<Env::Api>>,
+    >(
+        self,
+        value: Arg0,
+    ) -> TxTypedCall<Env, From, To, NotPayable, Gas, ()> {
+        self.wrapped_tx
+            .payment(NotPayable)
+            .raw_call("add")
+            .argument(&value)
+            .original_result()
+    }
+}

contracts/parametric-tests/adder-pt/src/adder_pt.rs

@@ -0,0 +1,91 @@
+#![no_std]
+
+mod adder_proxy;
+
+multiversx_sc::imports!();
+
+static INIT_SUM: u32 = 5u32;
+
+#[multiversx_sc::contract]
+pub trait TestAdder {
+    #[storage_mapper("ownerAddress")]
+    fn owner_address(&self) -> SingleValueMapper<ManagedAddress>;
+
+    #[storage_mapper("adderAddress")]
+    fn adder_address(&self) -> SingleValueMapper<ManagedAddress>;
+
+    /// Create the owner account and deploy adder
+    #[init]
+    fn init(&self, code_path: ManagedBuffer) {
+        // create the owner account
+        let owner = ManagedAddress::from(b"owner___________________________");
+        self.owner_address().set(&owner);
+
+        self.test_raw()
+            .create_account(&owner, 1, &BigUint::from(0u64));
+
+        // register an address for the contract to be deployed
+        let adder = ManagedAddress::from(b"adder___________________________");
+        self.test_raw().register_new_address(&owner, 1, &adder);
+
+        let adder = self
+            .tx()
+            .from(&owner)
+            .typed(adder_proxy::AdderProxy)
+            .init(INIT_SUM)
+            .code_path(code_path)
+            .gas(5000000000000)
+            .returns(ReturnsNewManagedAddress)
+            .test_deploy();
+
+        // save the deployed contract's address
+        self.adder_address().set(&adder);
+
+        // check the initial sum value
+        let sum: BigUint = self.storage_raw().read_from_address(&adder, "sum");
+        self.test_raw().assert(sum == INIT_SUM);
+    }
+
+    // Make a call from 'owner' to 'adder' and check the sum value
+    #[endpoint(test_call_add)]
+    fn test_call_add(&self, value: BigUint) {
+        self.test_raw().assume(value <= 100u32);
+
+        let adder = self.adder_address().get();
+
+        self.call_add(&value);
+
+        // check the sum value
+        let sum: BigUint = self.storage_raw().read_from_address(&adder, "sum");
+        self.test_raw().assert(sum == (value + INIT_SUM));
+    }
+
+    #[endpoint(test_call_add_twice)]
+    fn test_call_add_twice(&self, value1: BigUint, value2: BigUint) {
+        self.test_raw().assume(value1 <= 100u32);
+        self.test_raw().assume(value2 <= 100u32);
+
+        let adder = self.adder_address().get();
+
+        self.call_add(&value1);
+        self.call_add(&value2);
+
+        // check the sum value
+        let sum: BigUint = self.storage_raw().read_from_address(&adder, "sum");
+        self.test_raw().assert(sum == (value1 + value2 + INIT_SUM));
+    }
+
+    fn call_add(&self, value: &BigUint) {
+        let owner = self.owner_address().get();
+        let adder = self.adder_address().get();
+
+        // start a prank and call 'adder' from 'owner'
+        self.tx()
+            .from(owner)
+            .to(adder)
+            .typed(adder_proxy::AdderProxy)
+            .add(value)
+            .gas(5000000)
+            .test_call();
+    }
+}