Skip to content

Commit

Permalink
Foundry-like tests (#111)
Browse files Browse the repository at this point in the history 
* experiments for foundry-like parametric tests

* TestAdder contract and api functions

* basic foundry semantics

* run-elrond-tests.py => run_elrond_tests.py

* WrappedBytes in MapBytesToBytes and ListBytes

* test-adder.wat:keep function names

* add initial script to run tests with concrete execution

* add property-based testing with hypothesis

* temp

* temp

* add claim generator

* add error cases for foundry rules

* multisig test

* increase recursion limit

* foundryGetStorage returns empty bytes if not found

* use _kast for parsing/unparsing

* fix wrapped bytes

* after review: cleanup and add types

* make testapi.rs a cargo package

* codeHandle => codePathHandle

* fix recursion limit and refactor kast/krun

* add foundry tutorial to README.md

* split foundry assert rule

* implement foundry assume without ensures
  • Loading branch information
@bbyalcinkaya
bbyalcinkaya authored Aug 21, 2023
1 parent 402eeb6 commit 304113e
Show file tree
Hide file tree
Showing 46 changed files with 9,190 additions and 123 deletions.
2 changes: 2 additions & 0 deletions .gitignore
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,3 +9,5 @@
.kompile*

*.pyc
venv
.hypothesis
36 changes: 28 additions & 8 deletions Makefile
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@

.PHONY: all clean deps wasm-deps \
build build-llvm build-haskell \
plugin-deps libff libcryptopp libsecp256k1 \
build build-llvm build-haskell build-foundry \
plugin-deps libff libcryptopp libsecp256k1 \
elrond-clean-sources elrond-loaded \
test unittest-python mandos-test test-elrond-contracts \
test-elrond-adder test-elrond-crowdfunding-esdt \
Expand Down Expand Up @@ -111,7 +111,9 @@ $(libsecp256k1_out): $(PLUGIN_SUBMODULE)/deps/secp256k1/autogen.sh
&& $(MAKE) \
&& $(MAKE) install

plugin-deps: libff libcryptopp libsecp256k1
PLUGIN_DEPS := $(libff_out) $(libcryptopp_out) $(libsecp256k1_out)

plugin-deps: $(PLUGIN_DEPS)

# Build Dependencies (K Submodule)
# --------------------------------
Expand All @@ -136,7 +138,7 @@ endif
LLVM_KOMPILE_OPTS := -L$(LOCAL_LIB) \
-I$(LOCAL_INCLUDE) \
-I/usr/include \
$(PLUGIN_SUBMODULE)/plugin-c/plugin_util.cpp \
$(PLUGIN_SUBMODULE)/plugin-c/plugin_util.cpp \
$(PLUGIN_SUBMODULE)/plugin-c/crypto.cpp \
$(PLUGIN_SUBMODULE)/plugin-c/blake2.cpp \
-g -std=c++17 -lff -lcryptopp -lsecp256k1 \
Expand All @@ -152,6 +154,7 @@ ELROND_FILE_NAMES := elrond.md \
esdt.md \
auto-allocate.md \
mandos.md \
foundry.md \
$(wildcard data/*.k) \
$(wildcard vmhooks/*.md)

Expand All @@ -170,16 +173,16 @@ llvm_kompiled := $(llvm_dir)/mandos-kompiled/interpreter

build-llvm: $(llvm_kompiled)

$(llvm_kompiled): $(ELROND_FILES_KWASM_DIR) $(PLUGIN_FILES_KWASM_DIR) plugin-deps
$(llvm_kompiled): $(ELROND_FILES_KWASM_DIR) $(PLUGIN_FILES_KWASM_DIR) $(PLUGIN_DEPS)
$(KWASM_MAKE) build-llvm \
DEFN_DIR=../../$(DEFN_DIR)/$(SUBDEFN) \
llvm_main_module=$(MAIN_MODULE) \
llvm_syntax_module=$(MAIN_SYNTAX_MODULE) \
llvm_main_file=$(MAIN_DEFN_FILE) \
EXTRA_SOURCE_FILES="$(EXTRA_SOURCES)" \
KOMPILE_OPTS="$(KOMPILE_OPTS)" \
LLVM_KOMPILE_OPTS="$(LLVM_KOMPILE_OPTS)" \
K_INCLUDE_DIR=$(K_INCLUDE_DIR)
LLVM_KOMPILE_OPTS="$(LLVM_KOMPILE_OPTS)" \
K_INCLUDE_DIR=$(K_INCLUDE_DIR)

$(KWASM_SUBMODULE)/%.md: %.md
cp $< $@
Expand All @@ -196,6 +199,23 @@ $(KWASM_SUBMODULE)/data/%.k: data/%.k
@mkdir -p $(dir $@)
cp $< $@

# Foundry Build
foundry_kompiled := $(llvm_dir)/foundry-kompiled/interpreter

build-foundry: $(foundry_kompiled)

# runs llvm-kompile separately to reduce max memory usage
$(foundry_kompiled): $(ELROND_FILES_KWASM_DIR) $(PLUGIN_FILES_KWASM_DIR) $(PLUGIN_DEPS)
$(KWASM_MAKE) build-llvm \
DEFN_DIR=../../$(DEFN_DIR)/$(SUBDEFN) \
llvm_main_module=FOUNDRY \
llvm_syntax_module=FOUNDRY-SYNTAX \
llvm_main_file=foundry \
EXTRA_SOURCE_FILES="$(EXTRA_SOURCES)" \
KOMPILE_OPTS="$(KOMPILE_OPTS)" \
LLVM_KOMPILE_OPTS="$(LLVM_KOMPILE_OPTS)" \
K_INCLUDE_DIR=$(K_INCLUDE_DIR)

# Testing
# -------

Expand Down Expand Up @@ -243,7 +263,7 @@ $(ELROND_LOADED_JSON): $(ELROND_RUNTIME)
# Elrond Tests
# ------------

TEST_MANDOS := python3 run-elrond-tests.py
TEST_MANDOS := python3 run_elrond_tests.py


## Mandos Test
Expand Down
136 changes: 131 additions & 5 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ Semantics of Elrond and Mandos

This repository is work-in-progress, and currently a fork of [KWasm](https://github.com/kframework/wasm-semantics).

Elrond-specific code is in `elrond.md` and `run-elrond-tests.py`.
Elrond-specific code is in `elrond.md` and `run_elrond_tests.py`.

## Installation

Expand Down Expand Up @@ -53,10 +53,10 @@ $ mxpy contract build "<path-to-contract-directory>" --wasm-symbols
Then run Mandos scenarios with:

```shell
$ python3 run-elrond-tests.py <path-to-mandos-file>
$ python3 run_elrond_tests.py <path-to-mandos-file>
```

__Important__: `run-elrond-tests.py` makes use of Python modules implemented in the `wasm-semantics` submodule. For the time being, it requires setting the `PYTHONPATH` environment variable.
__Important__: `run_elrond_tests.py` makes use of Python modules implemented in the `wasm-semantics` submodule. For the time being, it requires setting the `PYTHONPATH` environment variable.

```shell
$ export PYTHONPATH=$(pwd)/deps/wasm-semantics/binary-parser:$PYTHONPATH
Expand All @@ -69,7 +69,7 @@ $ mxpy contract build "deps/mx-sdk-rs/contracts/examples/multisig" --wasm-symbol
...
INFO:projects.core:Build ran.
INFO:projects.core:WASM file generated: /path/to/multisig/output/multisig.wasm
$ python3 run-elrond-tests.py deps/mx-sdk-rs/contracts/examples/multisig/scenarios/changeBoard.scen.json
$ python3 run_elrond_tests.py deps/mx-sdk-rs/contracts/examples/multisig/scenarios/changeBoard.scen.json
```

## Rule Coverage
Expand All @@ -96,4 +96,130 @@ deps/wasm-semantics/elrond-config.md:324:10
...
```

The coverage files generated by `krun` are located under the build directory (`.build/defn/llvm/mandos-kompiled`). To clean up the coverage data generated, run `make clean-coverage`.
The coverage files generated by `krun` are located under the build directory (`.build/defn/llvm/mandos-kompiled`). To clean up the coverage data generated, run `make clean-coverage`.

## Writing Foundry-like Parametric Tests

### Create a test contract

To begin writing tests for your smart contract, you'll first need to create an empty contract using __mxpy__.

```shell
mxpy contract new --template empty test_adder
```

Next, add [`testapi`](./src/testapi) as a dependency to your project. This package contains auxiliary external functions specifically designed for testing, implemented as WASM host functions.

```
$ cargo add <path to src/testapi/>
```

### Initializing the test contract

The testing API provides the test contract with special abilities that regular contracts do not have, such as accessing the storage of other contracts and deploying contracts using local WASM file paths.

We will use the `init` function to deploy the contract(s) involved in our test cases and create an initial state for running the test cases. This can be thought of as the equivalent of the `setState` and `scDeploy` steps in scenario tests.

```rs
fn init(&self, code_path: ManagedBuffer)
```

The `init` function takes a path to the contract's wasm file as an argument and utilizes the `testapi::deploy_contract function` to deploy it. This function works similarly to the `scDeploy` step in the scenario format.

```rs
let adder = testapi::deploy_contract(
&owner, // address of the owner account
5000000000000, // some gas
&BigUint::zero(), // value
&code_path, // path to wasm file
&adder_init_args,
);
self.adder_address().set(&adder);
```

Once you've implemented the init function, it's essential to make sure the test runner knows the correct file path to use when deploying the test contract. To achieve this, you'll need to create a `foundry.json` file in the root directory of your test contract. In this file, specify the relative path to the contract's WASM file that you want to deploy for testing.

For example, assuming your test contract is named `test_adder`, and you want to deploy the `adder.wasm` contract located in the ../../../deps/mx-sdk-rs/contracts/examples/adder/output/ directory, your `foundry.json` file should look like this:

```json
{
"contract_paths": [
"../mx-sdk-rs/contracts/examples/adder/output/adder.wasm"
]
}
```

By providing the correct file path in the `foundry.json` file, the test runner will be able to deploy the specified contract during the testing process. With the `init` function in place and the contract file path specified, you are now ready to write test cases in endpoints.

### Writing test cases in endpoints

In our testing approach, test cases are organized as endpoints, clearly labeled with the 'test_' prefix for easy identification.

```rs
#[endpoint(test_call_add)]
fn test_call_add(&self, value: BigUint)
```

These endpoints can accept parameters, enabling us to express the contract's properties parametrically by varying these variables. This flexibility allows us to execute tests with fuzzing techniques or prove them using symbolic execution.

Within each endpoint, we interact with the contract deployed during the `init` phase and employ the testing API to make specific assertions. These assertions serve as validation checks, ensuring that the contract behaves as intended and produces the expected outcomes during testing.

In certain testing scenarios, it becomes necessary to simulate actions from another account. To achieve this, we employ a feature known as "pranks."

Pranks enable the test contract to act as another account temporarily. We initiate a prank by using the `testapi::start_prank(&acct_addr)` function, where `acct_addr` represents the address of the account we wish to impersonate. Once the prank is started, any calls made by the test contract will be executed as if they were sent from the specified `acct_addr`. This allows us to test various functionalities from the perspective of that particular account.

For instance, let's consider the following code snippet:

```rs
testapi::start_prank(&owner);
let res = self.send_raw().direct_egld_execute(
&adder,
&BigUint::from(0u32),
5000000,
&ManagedBuffer::from(b"add"),
&adder_init_args,
);
testapi::stop_prank();
```

In this example, we initiate a prank using the `owner` account address. Subsequently, we execute a call to the contract `adder` as if it were invoked from the `owner` account. Once the intended actions are completed, we stop the prank using `testapi::stop_prank()`.

After executing the call to the `adder` contract through a prank, it's common to observe changes in the contract's storage. To verify whether the expected changes have occurred, we can access the storage of the account using `testapi::get_storage`. In the following code snippet, we retrieve the value stored under the key "sum" in the storage of the `adder` contract:

```rs
let sum_as_bytes = testapi::get_storage(&adder, &ManagedBuffer::from(b"sum"));
let sum = BigUint::from(sum_as_bytes);
```

Once we have obtained the stored value, we can then proceed to make assertions to verify its correctness. In this example, we are checking if the `sum` value is equal to the sum of the initial value (`INIT_SUM`) and the current `value`:

```rs
testapi::assert(sum == (value + INIT_SUM));
```

By combining pranks with storage access and assertions, we can comprehensively test the behavior of our Smart Contracts, ensuring their accuracy and robustness in various scenarios.

### Running tests

To run the tests for your Smart Contracts, ensure that you have fulfilled the following prerequisites:

1. Compile the semantics by executing `make build-foundry`.
2. Compile the contract using `mxpy contract build <path to adder contract>`.
3. Install the `hypothesis` library by running `pip3 install hypothesis`. This library will be utilized for concrete execution with fuzzing.

Now, follow these steps to run the test contract:

Build the test contract by executing
```shell
mxpy contract build <path to test contract>
```

Run the `run_foundry.py` script with the test contract's path as the argument:

```shell
python3 run_foundry.py --directory <path to test contract>
```

The `run_foundry.py` script will deploy the test contract using the arguments specified in the `foundry.json` file located in the test directory. It will extract the names and argument types of the test endpoints. Subsequently, the script will test these endpoints using random inputs generated with the `hypothesis` library, enabling fuzz testing. If it encounters an input that falsifies the assertions made in the test cases, it attempts to shrink the input and identify a minimal failing example.

By following these steps, you can efficiently and comprehensively evaluate your Smart Contracts, ensuring their correctness and reliability in various scenarios and inputs.
11 changes: 11 additions & 0 deletions data/bytes-type.k
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@

module BYTES-TYPE
import BYTES

syntax WrappedBytes
syntax BYTES

syntax WrappedBytes ::= wrap(Bytes) [symbol, klabel(wrapBytes)]
syntax Bytes ::= unwrap(WrappedBytes) [function, total, injective, symbol, klabel(unwrapBytes)]
rule unwrap(wrap(A:Bytes)) => A
endmodule
47 changes: 33 additions & 14 deletions data/list-bytes.k
View file
Original file line number Diff line number Diff line change
@@ -1,8 +1,11 @@
requires "bytes-type.k"

module LIST-BYTES
imports private INT-SYNTAX
imports private BASIC-K


imports BYTES-TYPE

syntax Bytes

syntax ListBytes [hook(LIST.List)]
Expand All @@ -16,23 +19,23 @@ module LIST-BYTES
[ function, total, hook(LIST.unit), klabel(.ListBytes),
symbol, smtlib(smt_seq_nil), latex(\dotCt{ListBytes})
]
syntax ListBytes ::= ListItem(Bytes)
syntax ListBytes ::= ListItem(WrappedBytes)
[ function, total, hook(LIST.element), klabel(ListBytesItem),
symbol, smtlib(smt_seq_elem)
]
syntax Bytes ::= ListBytes "[" Int "]"
syntax WrappedBytes ::= ListBytes "[" Int "]"
[ function, hook(LIST.get), klabel(ListBytes:get), symbol ]
syntax ListBytes ::= ListBytes "[" index: Int "<-" value: Bytes "]"
syntax ListBytes ::= ListBytes "[" index: Int "<-" value: WrappedBytes "]"
[function, hook(LIST.update), klabel(ListBytes:set)]
syntax ListBytes ::= makeListBytes(length: Int, value: Bytes)
syntax ListBytes ::= makeListBytes(length: Int, value: WrappedBytes)
[function, hook(LIST.make)]
syntax ListBytes ::= updateList(dest: ListBytes, index: Int, src: ListBytes)
[function, hook(LIST.updateAll)]
syntax ListBytes ::= fillList(ListBytes, index: Int, length: Int, value: Bytes)
syntax ListBytes ::= fillList(ListBytes, index: Int, length: Int, value: WrappedBytes)
[function, hook(LIST.fill)]
syntax ListBytes ::= range(ListBytes, fromFront: Int, fromBack: Int)
[function, hook(LIST.range), klabel(ListBytes:range), symbol]
syntax Bool ::= Bytes "in" ListBytes
syntax Bool ::= WrappedBytes "in" ListBytes
[function, total, hook(LIST.in), klabel(_inListBytes_)]
syntax Int ::= size(ListBytes)
[function, total, hook(LIST.size), klabel (sizeListBytes), smtlib(smt_seq_len)]
Expand All @@ -42,24 +45,40 @@ module LIST-BYTES-EXTENSIONS
imports BOOL
imports INT
imports LIST-BYTES
imports BYTES-TYPE

syntax Bytes ::= ListBytes "[" Int "]" "orDefault" Bytes
syntax WrappedBytes ::= ListBytes "[" Int "]" "orDefault" WrappedBytes
[ function, total, klabel(ListBytes:getOrDefault), symbol ]

rule ListItem(V:Bytes) _:ListBytes [0] orDefault _:Bytes
syntax Bytes ::= ListBytes "{{" Int "}}"
[function, klabel(ListBytes:primitiveLookup)]
// -----------------------------------------------------------
rule L:ListBytes {{ I:Int }} => unwrap( L[ I ] )

syntax Bytes ::= ListBytes "{{" Int "}}" "orDefault" Bytes
[ function, total, klabel(ListBytes:primitiveLookupOrDefault) ]
// -----------------------------------------------------------------------------
rule L:ListBytes {{ I:Int }} orDefault Value:Bytes
=> unwrap( L [I] orDefault wrap(Value) )

rule ListItem(V:WrappedBytes) _:ListBytes [0] orDefault _:WrappedBytes
=> V
rule _:ListBytes ListItem(V:Bytes) [-1] orDefault _:Bytes
rule _:ListBytes ListItem(V:WrappedBytes) [-1] orDefault _:WrappedBytes
=> V
rule .ListBytes [_:Int] orDefault D:Bytes => D
rule .ListBytes [_:Int] orDefault D:WrappedBytes => D

rule ListItem(_:Bytes) L:ListBytes [I:Int] orDefault D:Bytes
rule ListItem(_:WrappedBytes) L:ListBytes [I:Int] orDefault D:WrappedBytes
=> L[I -Int 1] orDefault D
requires 0 <Int I
rule L:ListBytes ListItem(_:Bytes) [I:Int] orDefault D:Bytes
rule L:ListBytes ListItem(_:WrappedBytes) [I:Int] orDefault D:WrappedBytes
=> L[I +Int 1] orDefault D
requires I <Int 0

rule L:ListBytes[I:Int] orDefault D:Bytes => D
rule L:ListBytes[I:Int] orDefault D:WrappedBytes => D
requires notBool (0 -Int size(L) <=Int I andBool I <Int size(L))
[simplification]

syntax ListBytes ::= ListItemWrap( Bytes ) [function, total, klabel(ListBytesItemWrap)]
rule ListItemWrap( B:Bytes ) => ListItem(wrap(B))

endmodule
Loading

0 comments on commit 304113e

Please sign in to comment.