Skip to content

Commit 3a5c82f

Browse files
ehildenbgtrepta
andauthored
Documentation Updates (#236)
* INSTALL: remove instructions for installing curl * INSTALL: update build from source instructions * README: update README instructions * README: add example of running haskell backend * README: typos Co-authored-by: gtrepta <[email protected]> * README: document iele-binary and iele-node Co-authored-by: gtrepta <[email protected]>
1 parent 40ad489 commit 3a5c82f

File tree

2 files changed

+118
-108
lines changed

2 files changed

+118
-108
lines changed

INSTALL.md

Lines changed: 11 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -67,21 +67,7 @@ It is safe to skip any of these dependencies that are already installed.
6767
Follow the instructions below.
6868
Perform all steps as your normal (non-root) user.
6969
You may find the same instructions and our public key at <https://runtimeverification.cachix.org>.
70-
71-
#### curl
72-
73-
Install curl using your distribution's package manager:
74-
75-
```.sh
76-
# Ubuntu and Debian
77-
sudo apt install curl
78-
79-
# Fedora, RHEL, and CentOS
80-
sudo yum install curl
81-
82-
# Arch Linux
83-
sudo pacman -Sy curl
84-
```
70+
To follow this instructions, you will need `curl` installed on your system <https://curl.haxx.se/download.html>.
8571

8672
#### Nix
8773

@@ -153,14 +139,20 @@ curl -sSL https://get.haskellstack.org/ | sh
153139
These commands build and install K and KIELE:
154140

155141
```sh
156-
git clone git@github.com:runtimeverification/iele-semantics.git
142+
git clone https://github.com/runtimeverification/iele-semantics.git
157143
cd iele-semantics
158144
git submodule update --init --recursive
159-
curl -sSL https://github.com/kframework/k/releases/download/$(cat deps/k_release)/kframework_5.0.0_amd64_bionic.deb
160-
sudo apt-get install --yes ./kframework_5.0.0_amd64_bionic.deb
145+
curl -sSL https://github.com/kframework/k/releases/download/$(cat deps/k_release)/kframework_5.0.0_amd64_bionic.deb --output kframework.deb
146+
sudo apt-get install --yes ./kframework.deb
161147
sudo bash -c 'OPAMROOT=/usr/lib/kframework/opamroot k-configure-opam'
162148
sudo bash -c 'OPAMROOT=/usr/lib/kframework/opamroot opam install --yes ocaml-protoc rlp yojson zarith hex uuidm cryptokit'
163149
export OPAMROOT=/usr/lib/kframework/opamroot
164150
eval $(opam config env)
165-
make COVERAGE=k
151+
make build -j4
152+
```
153+
154+
Finally, set the install directory on PATH:
155+
156+
```sh
157+
export PATH=$(pwd)/.build/lib:$PATH
166158
```

README.md

Lines changed: 107 additions & 89 deletions
Original file line numberDiff line numberDiff line change
@@ -5,124 +5,142 @@ In this repository we provide a model of IELE in K.
55

66
### Structure
77

8-
The file [iele-syntax.md](iele-syntax.md) contains the syntax definition of IELE, along with comments that guide the reader through the structure of the language and links to more detailed descriptions of various features. This file is a good starting point for getting familiar with the language.
9-
10-
The file [data.md](data.md) explains the basic data of IELE (including words and some datastructures over them).
11-
This data is defined functionally.
12-
13-
[iele.md](iele.md) is the file containing the semantics of IELE.
14-
This file contains the **configuration** (a map of the state), and a simple imperative execution machine which IELE lives on top of.
15-
It deals with the semantics of opcodes and parsing/unparsing/assembling/disassembling.
16-
17-
[iele-gas.md](iele-gas.md) describes gas price computations. [iele-gas-summary.md](iele-gas-summary.md) summarizes them in a format readable by those who don't know K.
18-
19-
Finally, the file [Design.md](Design.md) discusses the design rationale of IELE. It also provides more detailed descriptions of various IELE features, as well as differences and similarities with EVM and LLVM.
20-
21-
### Testing
22-
23-
[iele-testing.md](iele-testing.md) loads test-files from the [Ethereum Test Set](https://github.com/ethereum/tests) and executes them, checking that the output is correct.
24-
If the output is correct, the entire configuration is cleared.
25-
If any check fails, the configuration retains the failed check at the top of the `<k>` cell.
26-
27-
[iele-testing.md](iele-testing.md) is also capable of executing tests of arbitrary IELE transactions (subject to the fact that this first release of IELE is still
28-
built on top of an ethereum-like network layer). The test format is based off of, but slightly different from, the ethereum BlockchainTest json test format.
29-
30-
The structure of the json files is as follows:
31-
32-
* The top level is a json object, containing a list of key value pairs whose keys are the names of the tests to be executed and whose values are json objects containing an individual test case. The top-level fields in each test case are described below:
33-
* "pre": a json object mapping account IDs (20-byte hexadecimal strings) to an object for each account representing the state of that account before the test starts.
34-
* "blocks": a list of blocks the test should execute, each containing the folowing fields:
35-
* "transactions": a list of transactions to be executed, each containing the following fields:
36-
* "nonce": the nonce of the sender of the transaction.
37-
* "function": the name of the function to be called. Should be the empty string if the "to" field is the empty string.
38-
* "gasLimit": the gas limit of the transaction.
39-
* "value": the amount of currency sent with the transaction.
40-
* "to": the account the transaction is calling a function on. If the transaction creates an account, this field should be the empty string.
41-
* "arguments": a list of integers representing the input arguments of the top-level function call of the transaction.
42-
* "contractCode": the contract being uploaded. Should be the empty string if the "to" field is NOT the empty string.
43-
* "gasPrice": the price to be paid per unit of gas used.
44-
* "secretKey" OR ("v" AND "r" AND "s"): the signature of the transaction (either as a private key or as an ECDSA signature of the remaining fields) used to sign the transaction.
45-
* "results": a list of results of each transaction in the block, each containing the following fields:
46-
* "out": a list of integers representing the output of the top-level function call of the transaction.
47-
* "status": the exit status of the top-level function call of the transaction.
48-
* "gas": the amount of gas remaining after the transaction executes.
49-
* "logs": the keccak256 hash of the rlp-encoded log entries generated by the transaction.
50-
* "refund": the gas refund after the transaction executes.
51-
* "blockHeader": a json object containing the partial block header of the current block, with the following fields:
52-
* "gasLimit": The block gas limit.
53-
* "number": The block number.
54-
* "difficulty": The block difficulty.
55-
* "timestamp": The timestamp of the block.
56-
* "coinbase": The block's beneficiary.
57-
* "network": The current network rules. Currently only one ruleset is supported, "Albe".
58-
* "blockhashes": because we don't specify the entire blocks, it is necessary to explicitly specify the information seen by the iele.blockhash function. This should be a list of 32-byte hashes ending in 0x00 representing the parentHash of the genesis block.
59-
* "postState": a json object mapping accoutn IDs (20-byte hexadecimal strings) to an object for each account representing the state of that account expected after the test finishes.
60-
61-
* Each account listed in the "pre" or "postState" fields has the following fields:
62-
* "nonce": the nonce of the account.
63-
* "balance": the balance of currency in the account.
64-
* "storage": a json object mapping integer storage keys to integer storage values.
65-
* "code": either "", representing an empty account, a string beginning with "0x", indicating a binary representation of an account, or a filename containing a IELE contract to be assembled and used as the code of the account.
66-
67-
* Each integer is encocded as a string in hexadecimal representing the big-endian representation of the integer. The empty string also can be used to represent the integer zero.
68-
69-
For example pure-IELE tests, see `tests/iele`.
8+
- The file [iele-syntax.md](iele-syntax.md) contains the syntax definition of IELE, along with comments that guide the reader through the structure of the language and links to more detailed descriptions of various features.
9+
This file is a good starting point for getting familiar with the language.
10+
- The file [data.md](data.md) explains the basic data of IELE (including words and some datastructures over them).
11+
This data is defined functionally.
12+
- [iele.md](iele.md) is the file containing the semantics of IELE.
13+
This file contains the **configuration** (a map of the state), and a simple imperative execution machine which IELE lives on top of.
14+
It deals with the semantics of opcodes and parsing/unparsing/assembling/disassembling.
15+
- [iele-gas.md](iele-gas.md) describes gas price computations. [iele-gas-summary.md](iele-gas-summary.md) summarizes them in a format readable by those who don't know K.
16+
- [iele-binary.md](iele-binary.md) defines the mnemonic for each opcode, and the disassembler.
17+
- [iele-node.md](iele-node.md) defines the protobuf communication protocol used to plug the IELE VM into anonther client to make a full node.
18+
- [iele-testing.md](iele-testing.md) loads test-files from the [Ethereum Test Set](https://github.com/ethereum/tests) and executes them, checking that the output is correct.
19+
If the output is correct, the entire configuration is cleared.
20+
If any check fails, the configuration retains the failed check at the top of the `<k>` cell.
21+
[iele-testing.md](iele-testing.md) is also capable of executing tests of arbitrary IELE transactions (subject to the fact that this first release of IELE is still built on top of an ethereum-like network layer).
22+
The test format is based off of, but slightly different from, the ethereum BlockchainTest json test format.
7023

7124
Using the Definition
7225
--------------------
7326

74-
### Installing
27+
### Installing/Building
7528

7629
See [INSTALL.md](INSTALL.md).
7730

78-
### Testing
31+
### Help/Version
7932

80-
To execute a VM test, run `./vmtest $file` where `$file` is a JSON file containing the specification of the test.
81-
To execute a Blockchain test, run `./blockchaintest $file` where `$file` is a JSON file containing the specification of the test.
33+
Calling `kiele help` and `kiele version` will output the user guide and the KIELE version, respectively.
8234

83-
To run only the pure-IELE tests, run `make iele-test`.
35+
### Assembler
8436

85-
For testing the interprocess VM API, first start the vm server
86-
by running `.build/vm/iele-vm 10000 127.0.0.1` in another shell or
87-
in the background.
88-
With the server running, run `make iele-test-node` to run the pure-IELE
89-
tests on the vm server, or run individual tests using `.build/vm/iele-vm-test`.
37+
The assembler takes textual IELE and produces IELE bytecode.
38+
For example, on the following file `iele-examples/factorial.iele`:
9039

91-
To execute all currently passing tests, run `make test`. Note that the vm server should have been started for `make test` to succeed.
40+
```iele
41+
contract Factorial {
9242
93-
### Debugging
43+
define public @factorial(%n) {
44+
%lt = cmp lt %n, 0
45+
br %lt, throw
9446
95-
When executing a test, if a test fails, the intermediate state of the IELE VM is dumped on the command line. This can be used to provide
96-
information about exactly what went wrong with the test, which can be used for debugging purposes. Generally speaking, each dumped state begins with
97-
the string `` `<generatedTop>`(`<k>` `` followed by the current list of instructions to be executed by the VM in balanced parentheses. You can usually
98-
determine what went wrong with the test by examining the first entry in the list (i.e., everything up to the first `~>`).
47+
%result = 1
9948
100-
Some examples of common errors you may encounter are below, with each example followed by a description of the error.
49+
condition:
50+
%cond = cmp le %n, 0
51+
br %cond, after_loop
10152
53+
loop_body:
54+
%result = mul %result, %n
55+
%n = sub %n, 1
56+
br condition
57+
58+
after_loop:
59+
ret %result
60+
61+
throw:
62+
call @iele.invalid()
63+
}
64+
65+
define @init() {}
66+
}
10267
```
103-
loadTx(#token("966588469268559010541288244128342317224451555083","Int"))
68+
69+
You can run:
70+
71+
```sh
72+
kiele assemble iele-examples/factorial.iele
10473
```
10574

106-
In this example, either a transaction was signed incorrectly, or the sender of the transaction as specified by its signature does not exist.
75+
To produce output:
10776

77+
```sh
78+
0000004C6303690009666163746F7269616C6800010001618001100042650003026101036600006180011200446500020466000102001B610101030040640000660002F6000103660003FE6700000000
10879
```
109-
`check__IELE-TESTING`(`_:__IELE-DATA`(#token("\"account\"","String"),`{_}_IELE-DATA`(`_,__IELE-DATA`(`_:__IELE-DATA`(#token("91343852333181432387730302044767688728495783936","Int"),`{_}_IELE-DATA`(`_,__IELE-DATA`(`_:__IELE-DATA`(#token("\"storage\"","String"),`_Map_`(`_|->_`(#token("0","Int"),#token("10001","Int")),`_|->_`(#token("2428090106599461928744973076844625336880384098059","Int"),#token("10000","Int")))),`.List{"_,__IELE-DATA"}`(.KList)))),`.List{"_,__IELE-DATA"}`(.KList)))))
80+
81+
**NOTE**: Right now, if you use the NixOS package, you must call `iele-assemble` instead of `kiele assemble`.
82+
83+
### KIELE Node
84+
85+
You can run a KIELE node, specifying the port to run on and use the KIELE test harness to run some transactions through it.
86+
To start the KIELE node, call (in one terminal):
87+
88+
```sh
89+
kiele vm --port 9001
11090
```
11191

112-
Here account 91343852333181432387730302044767688728495783936 (in decimal) has different values for storage than expected by the test. Similar errors exist for the nonce, balance, and code of an account. You can refer to the `<storage>` cell in the dumped state for information on their actual values. The correct storage cell is nested within an `<account>` cell whose `<acctID>` is the address of the account in decimal.
92+
Then in a separate terminal, send a transaction through:
11393

94+
```sh
95+
iele-test-vm tests/iele/danse/factorial/factorial_positive.iele.json 9001
11496
```
115-
`check__IELE-TESTING`(`_:__IELE-DATA`(#token("\"out\"","String"),`[_]_IELE-DATA`(`_,__IELE-DATA`(#token("\"0x01\"","String"),`.List{"_,__IELE-DATA"}`(.KList)))))
97+
98+
You'll see the launched node record to the terminal a list of messages it sends and receives.
99+
100+
**NOTE**: The `iele-test-vm` executable is only available in a from-source build of KIELE.
101+
You can still launch and use the KIELE VM node without this executable.
102+
103+
### Interpreter
104+
105+
Tests in the Ethereum Test Suite format can be run directly by the IELE interpreter.
106+
107+
For example, from this repository, you can run:
108+
109+
```sh
110+
make assemble-iele-test -j4
111+
```
112+
113+
To prepare the Ethereum test-suite.
114+
Then you can run an individual test, and see the post-state with:
115+
116+
```sh
117+
kiele interpret tests/iele/danse/factorial/factorial_positive.iele.json.test-assembled
118+
```
119+
120+
You may also run the interpreter with the Haskell backend instead (though it is significantly slower):
121+
122+
```sh
123+
kiele interpret --backend haskell tests/iele/danse/factorial/factorial_positive.iele.json.test-assembled
116124
```
117125

118-
Here is a similar error, but the error states that the transaction returned an incorrect list of values. The actual return value can be found in the `<output>` cell.
126+
**NOTE**: Printing the post-state will not work unless you are using a from-source build of KIELE.
127+
Instead, you should inspect the exit code of `kiele interpret` to see if the test passed or failed, by adding option `--no-unparse` to skip printing the post-state.
128+
129+
### Well-Formedness Checker
130+
131+
The KIELE well-formedness checker will do some type-checking on the input IELE program, using exit code to indicate success/failure.
132+
For example, we can type-check the ERC20 contract example `iele-examples/erc20.iele`:
133+
134+
```sh
135+
kiele check --schedule DANSE iele-examples/erc20.iele
136+
```
119137

120-
If other errors occur that are not on this list, feel free to contact us on Gitter or Riot and we will be happy to assist in helping you understand. Future releases of IELE may also have improved debugging information making this easier to interpret.
138+
**NOTE**: The KIELE well-formedness checker requires that (i) you are using a local build of KIELE, and (ii) you have installed K as well.
121139

122140
Contacting Us
123141
-------------
124142

125-
In the spirit of open source, community-driven development, we will be holding all IELE discussions on our channels:
143+
To reach us, you can either use our chat, or open issues against this repository:
126144

127-
* [#IELE:matrix.org](https://riot.im/app/#/room/#IELE:matrix.org) on [Riot](https://riot.im)
128-
* [runtimeverification/iele-semantics](https://gitter.im/runtimeverification/iele-semantics) for issues/pull-requests.
145+
- [#IELE Element Channel](https://app.element.io/#/room/!LtQJkJbwuhxaMuWVOa:matrix.org) for chat.
146+
- [runtimeverification/iele-semantics](https://github.com/runtimeverification/iele-semantics) for issues/pull-requests.

0 commit comments

Comments
 (0)