Skip to content

Commit d132c8c

Browse files
bbyalcinkayabbyalcinkaya
committed
remove the example from the home page
1 parent 19c4c30 commit d132c8c

File tree

1 file changed

+1
-187
lines changed

1 file changed

+1
-187
lines changed

‎README.md

+1-187
Original file line numberDiff line numberDiff line change
@@ -44,193 +44,7 @@ komet --help
4444

4545
## 2. Guides
4646

47-
### 2.1. Komet Example: Testing the `adder` Contract
48-
49-
(Source: https://github.com/runtimeverification/komet-demo)
50-
51-
To illustrate how Komet can be used to test Soroban contracts, let's look at a simple example. We'll be working with a basic contract called adder, which features a single function that adds two numbers and returns their sum. In Komet, we write our tests as contracts that interact with the contract we want to test. For this example, we will create a test_adder contract to verify the behavior of the adder contract.
52-
53-
The project structure for this example looks like this:
54-
55-
```
56-
.
57-
├── contracts
58-
│ ├── adder
59-
│ │ ├── src
60-
│ │ │ └── lib.rs
61-
│ │ └── Cargo.toml
62-
│ └── test_adder
63-
│ ├── src
64-
│ │ ├── lib.rs
65-
│ │ └── komet.rs
66-
│ ├── Cargo.toml
67-
│ └── kasmer.json
68-
├── Cargo.toml
69-
└── README.md
70-
```
71-
72-
#### The `adder` Contract
73-
74-
The adder contract is a simple, stateless contract with a single endpoint, add. This function takes two numbers as input and returns their sum. The result is returned as a u64 to avoid overflows. Since the contract doesn't maintain any internal state or use storage, its behavior is straightforward and purely based on the inputs provided.
75-
76-
```rust
77-
#![no_std]
78-
use soroban_sdk::{contract, contractimpl, Env};
79-
80-
#[contract]
81-
pub struct AdderContract;
82-
83-
#[contractimpl]
84-
impl AdderContract {
85-
pub fn add(_env: Env, first: u32, second: u32) -> u64 {
86-
first as u64 + second as u64
87-
}
88-
}
89-
```
90-
91-
### 2.2 Writing The Test Contract
92-
93-
Test contracts typically have an init function for setting up the initial state, such as deploying contracts or preparing the blockchain environment. They also include functions with names starting with test_ to define properties and run test cases against the contract being tested. Test contracts have special abilities that normal contracts do not, provided by our framework through custom WebAssembly hooks. These hooks, declared as extern functions in komet.rs, enable advanced operations like contract creation and state manipulation.
94-
95-
#### Setting the Initial State: The init Function
96-
97-
In the context of testing the adder contract, the init function is specifically responsible for deploying the adder contract and saving its address within the test contract's storage.
98-
99-
```rust
100-
#[contract]
101-
pub struct TestAdderContract;
102-
103-
#[contractimpl]
104-
impl TestAdderContract {
105-
pub fn init(env: Env, adder_hash: Bytes) {
106-
let addr_bytes = b"adder_ctr_______________________";
107-
let adder = komet::create_contract(&env, &Bytes::from_array(&env, addr_bytes), &adder_hash);
108-
env.storage().instance().set(&ADDR_KEY, &adder);
109-
}
110-
111-
// other functions
112-
}
113-
```
114-
115-
We are using the `create_contract` function from `komet.rs` for deploying a contract with a specified address and a Wasm hash. The hash represents the Wasm code of the target contract (in this case, the `adder` contract).
116-
117-
The contracts passed to `init` are specified in the `kasmer.json` file, where we provide the relative path to each contract. In this example, there is only one contract—the `adder` contract—but more complex tests may require multiple contracts. Komet locates and compiles each contract, registers the Wasm module, and passes its hash to the `init` function.
118-
119-
```json
120-
{
121-
"contracts": [
122-
"../adder"
123-
]
124-
}
125-
```
126-
127-
Komet will locate the `adder` contract, compile it to Wasm, and register the resulting Wasm module automatically.
128-
129-
If the contract requires a custom build process or is already precompiled, you can provide the path to the compiled Wasm file instead:
130-
131-
```json
132-
{
133-
"contracts": [
134-
"../../target/wasm32-unknown-unknown/release/adder.wasm"
135-
]
136-
}
137-
```
138-
139-
140-
#### Defining Contract Properties: test endpoints
141-
142-
In Komet, test cases are defined as contract endpoints with names starting with the test_ prefix. These endpoints specify properties of the contract being tested and return a boolean to indicate whether the test passed or failed.
143-
144-
For instance, in the test_adder contract, the test_add function verifies the adder contract's behavior by using its address—set up in the init function—to invoke the add method and check whether the adder contract correctly computes the sum of two numbers.
145-
146-
```rust
147-
impl TestAdderContract {
148-
// Initialization code...
149-
150-
pub fn test_add(env: Env, x: u32, y: u32) -> bool {
151-
// Retrieve the address of the `adder` contract from storage
152-
let adder: Address = env.storage().instance().get(&ADDR_KEY).unwrap();
153-
154-
// Create a client for interacting with the `adder` contract
155-
let adder_client = adder_contract::Client::new(&env, &adder);
156-
157-
// Call the `add` endpoint of the `adder` contract with the provided numbers
158-
let sum = adder_client.add(&x, &y);
159-
160-
// Check if the returned sum matches the expected result
161-
sum == x as u64 + y as u64
162-
}
163-
}
164-
```
165-
166-
### 2.3 Running Tests
167-
168-
Once the test contract is written, the next step is to compile and run it. Here's how you can execute the tests using Komet.
169-
170-
1. Navigate to the Test Contract Directory
171-
172-
After compiling the project, change directories into the `test_adder` contract folder:
173-
174-
```bash
175-
cd contracts/test_adder/
176-
```
177-
178-
2. Running Tests with Fuzzing
179-
180-
To run the tests using fuzzing (which generates random inputs for testing), use the following command:
181-
182-
```bash
183-
komet test
184-
```
185-
186-
After some compilation logs, you should see a progress bar:
187-
188-
<figure><img src=".gitbook/assets/komet-test-demo.gif" alt=""><figcaption></figcaption></figure>
189-
190-
This indicates that Komet discovered the `test_add` function and successfully executed the test using randomized inputs. By default, Komet runs each test 100 times. You can specify a different number of iterations using the `--max-examples` argument:
191-
192-
```bash
193-
komet test --max-examples 500
194-
```
195-
196-
This runs the test 500 times, allowing for more thorough fuzzing when needed.
197-
198-
3. Running Tests with Symbolic Execution (Proving)
199-
200-
To run tests with symbolic execution, which verifies the contract's behavior for all possible inputs, use the following command:
201-
202-
```bash
203-
komet prove run
204-
```
205-
206-
This method will run the proof for all test functions in the contract. It ensures that the property being tested holds true across all input combinations, providing thorough verification of the contract's correctness.
207-
208-
Additionally, you can explore more proving options by using the `--help` flag to see available commands and arguments:
209-
210-
```bash
211-
$ komet prove --help
212-
usage: komet prove [-h] [--always-allocate] [--node NODE] [--proof-dir PROOF_DIR] [--bug-report BUG_REPORT] [--extra-module EXTRA_MODULE] [--id ID] [--wasm WASM] [--directory DIRECTORY] COMMAND
213-
214-
positional arguments:
215-
COMMAND Proof command to run. One of (run, view, view-node, remove-node)
216-
217-
options:
218-
-h, --help show this help message and exit
219-
--always-allocate
220-
--node NODE
221-
--proof-dir PROOF_DIR
222-
Output directory for proofs
223-
--bug-report BUG_REPORT
224-
Bug report directory for proofs
225-
--extra-module EXTRA_MODULE
226-
Extra module with user-defined lemmas to include for verification (which must import KASMER module).Format is <file>:<module name>.
227-
--id ID Name of the test function in the testing contract
228-
--wasm WASM Use a specific contract wasm file instead
229-
--directory DIRECTORY, -C DIRECTORY
230-
The working directory for the command (defaults to the current working directory).
231-
```
232-
233-
After running the proof with the `--proof-dir` option, you can use the `view` command to inspect the proof tree and examine the details of symbolic execution.
47+
### [2.1. Komet Example: Testing the `adder` Contract](guides/komet-example/)
23448

23549
## 3. Real-World Demo
23650

0 commit comments

Comments
 (0)