| 25 Jan 2018 |
 johan andries (Gitter) | == kompile: .build/rvk/ethereum-kompiled/interpreter
tests/ci/rv-k/k-distribution/target/release/k/bin/kompile --debug --main-module ETHEREUM-SIMULATION \
--syntax-module IELE-SYNTAX .build/rvk/ethereum.k --directory .build/rvk \
--hook-namespaces KRYPTO --gen-ml-only -O3 --non-strict
/tmp/tmp-kompile-3368781429881838545.l:8611: warning, rule cannot be matched
/tmp/tmp-kompile-6690750962456022966.l:23824: warning, rule cannot be matched
40 states, 1247 transitions, table size 5228 bytes
ocamlfind opt -c .build/rvk/ethereum-kompiled/constants.ml -package gmp -package zarith
ocamlfind opt -c -I .build/rvk/ethereum-kompiled KRYPTO.ml -package cryptokit -package secp256k1 -package bn128
ocamlfind opt -a -o semantics.cmxa KRYPTO.cmx
ocamlfind remove iele-semantics-plugin
Removed /home/johan/.opam/4.03.0+k/lib/iele-semantics-plugin/META
Removed /home/johan/.opam/4.03.0+k/lib/iele-semantics-plugin
ocamlfind install iele-semantics-plugin META semantics.cmxa semantics.a KRYPTO.cmi KRYPTO.cmx
Installed /home/johan/.opam/4.03.0+k/lib/iele-semantics-plugin/KRYPTO.cmx
Installed /home/johan/.opam/4.03.0+k/lib/iele-semantics-plugin/KRYPTO.cmi
Installed /home/johan/.opam/4.03.0+k/lib/iele-semantics-plugin/semantics.a
Installed /home/johan/.opam/4.03.0+k/lib/iele-semantics-plugin/semantics.cmxa
Installed /home/johan/.opam/4.03.0+k/lib/iele-semantics-plugin/META
tests/ci/rv-k/k-distribution/target/release/k/bin/kompile --debug --main-module ETHEREUM-SIMULATION \
--syntax-module IELE-SYNTAX .build/rvk/ethereum.k --directory .build/rvk \
--hook-namespaces KRYPTO --packages iele-semantics-plugin -O3 --non-strict
/tmp/tmp-kompile-2644832360223680173.l:8611: warning, rule cannot be matched
/tmp/tmp-kompile-4648644375054646150.l:23824: warning, rule cannot be matched
40 states, 1247 transitions, table size 5228 bytes
File "realdef.ml", line 1:
Error: The files prelude.cmi
and /home/johan/.opam/4.03.0+k/lib/iele-semantics-plugin/KRYPTO.cmi
make inconsistent assumptions over interface Constants
org.kframework.utils.errorsystem.KEMException: [Error] Critical: ocamlopt returned nonzero exit code: 2
Examine output to see errors.
at org.kframework.utils.errorsystem.KEMException.create(KEMException.java:113)
at org.kframework.utils.errorsystem.KEMException.criticalError(KEMException.java:30)
at org.kframework.backend.ocaml.OcamlBackend.accept(OcamlBackend.java:110)
at org.kframework.kompile.KompileFrontEnd.run(KompileFrontEnd.java:71)
at org.kframework.main.FrontEnd.main(FrontEnd.java:52)
at org.kframework.main.Main.runApplication(Main.java:113)
at org.kframework.main.Main.runApplication(Main.java:103)
at org.kframework.main.Main.main(Main.java:52)
[Error] Critical: ocamlopt returned nonzero exit code: 2
Examine output to see errors.
Makefile:111: recipe for target '.build/rvk/ethereum-kompiled/interpreter' failed
make: * [.build/rvk/ethereum-kompiled/interpreter] Error 113 | 16:38:49 |
 dwight.guth | Can you please run `make clean; ocamlfind remove iele-semantics-plugin; make` and let me know if the problem recurs? | 17:07:48 |
| johan andries (Gitter) | Unfortunately the error remains. I checked to make sure the remove command did delete ~/.opam/4.03.0+k/lib/iele-semantics-plugin/KRYPTO.cmi. | 17:18:47 |
| dwight.guth | can you please try checking out the `install` branch and then rebuilding everything and let me know if you still have the problem? | 18:20:48 |
| dwight.guth | if that works I will merge those changes into the master branch, but I can't reproduce on my own so I'd like you to test first | 18:21:11 |
| johan andries (Gitter) | The changes in the install branch fixed the error. Thank you for your help. | 18:33:25 |
| 27 Jan 2018 |
|  ryan_stock joined the room. | 03:32:40 |
|  hatter6822 joined the room. | 18:50:55 |
| 19 Feb 2018 |
|  stakehub.io joined the room. | 02:19:16 |
| 15 Mar 2018 |
|  matekdk joined the room. | 00:25:00 |
| matekdk | Hello - I've spend some time looking at IELE - seems pretty solid :) Can I ask you - is this a project that is 'dedicated' to Cardano blockchain ? Or is the idea that other chains will pick this up ? | 00:26:36 |
| 16 Mar 2018 |
 Grigore | Hi matekdk . No, IELE is not dedicated to Cardano. But Cardano will likely be the first blockchain to adopt it. Note that IOHK funded the entire IELE project. We'd be glad to see IELE deployed on more blockchains in the future, though. | 02:59:49 |
| matekdk | Grigore: Cool - is there a specific person I should contact in that regard ? For possible biz-inquiries also - in regards to needed tweaks to iele. | 13:25:40 |
| Grigore | matekdk: you can always contact dwight.guth, @brandon.moore, @theo.kasampalis and myself (see https://runtimeverification.com/team/). We'd like to know what you plan to do with it. | 15:09:08 |
| matekdk | Grigore: Thanx - you guys will receive en email from me later. | 18:33:35 |
| 27 Mar 2018 |
|  @zhanla0:matrix.org joined the room. | 01:47:10 |
| @zhanla0:matrix.org | will a c++ blockchain work with iele? | 02:04:52 |
| @zhanla0:matrix.org | iele seems like a great project. I really am glad to see the industry moving away from ethereum dependence such as EVM. | 02:06:21 |
| dwight.guth | Iele has an open source inter process communication api for invoking the vm to execute a transaction, so code in any language can be used to interface with it if it follows that interface. The code is also under a very permissive open source license, so nothing is stopping you from implementing a iele vm in c++ either. | 04:06:30 |
| @zhanla0:matrix.org | great thanks! | 04:28:41 |
| 14 Apr 2018 |
|  hysnabi joined the room. | 12:17:42 |
| 22 Apr 2018 |
|  Greg Colvin joined the room. | 17:29:22 |
| Greg Colvin changed their display name from gcolvin to Greg Colvin. | 17:53:32 |
| Greg Colvin set a profile picture. | 17:56:53 |
| Greg Colvin removed their display name Greg Colvin. | 17:58:40 |
| Greg Colvin | 18:00:06 |
| 27 Apr 2018 |
|  jurajselep | simplestaking.com changed their display name from jurajselep to jurajselep(simplestaking.com). | 15:23:16 |
| 7 May 2018 |
|  Greg Colvin (Gitter) joined the room. | 18:38:25 |
| Greg Colvin (Gitter) | Some performance concerns.
- First, the arbitrary-precision arithmetic would seem to make it difficult to efficiently implement registers of fixed size with twos-complement wrap-around.
- Next, the flat-then-quadratic memory cost function doesn't work that well for the EVM, adding complexity without adding realism. Actual memory takes a few approximately exponential jumps through fast cache to RAM, then is flat again until it hits a wall when memory runs out. Perhaps a well-tuned function of the form y=a+b/(c+x) could give a flat start and a steep rise toward an asymptote.
- Worse, the operations for resizing memory take a fixed amount of gas per memory delta, but in real memory-management runtimes the time taken varies, and is a vulnerability. And memory management runtimes add unfortunate complexity to the VM.
| 18:38:32 |
 Grigore Rosu (Gitter) | Hi @gcolvin , nice to see you here. Thanks for your comments. We'll get back to you with some questions to see what your thoughts are about this.
Note that our main objective here was really to make formal verification of smart contracts easier. We verified a few on the EVM (https://github.com/runtimeverification/verified-smart-contracts) and we designed IELE with that experience in mind.
Like anything else, it is an experiment. We tried to come from the mathematical side, to have things clean there, and then worry about the (admittedly important) low-level details afterwards; that is, now :). | 18:54:58 |
