| 6 Sep 2018 |
 @gcolvin:matrix.org | Grigore, or whoever can answer. If I may ask again, as it's starting to matter to my EVM work. If I understand it, IELE registers are unbounded integers--their size changes to match the result of an operation. LLVM registers are bounded--their size is arbitrary but does not change. I'm wondering, Why the discrepancy?
I'm asking because EVM registers are bounded at 256 bits, with a few MOD operations to make it possible to work in a different fixed modulus fairly easily. But our current gas model does account for the size of the operands. I'm thinking that the IELE gas model can adapted to the EVM so that compilers so that compilers can take advantage of operand size and have that reflected in gas costs. That could save us the trouble of introducing new, narrow operations. | 17:51:29 |
| @gcolvin:matrix.org | "does account" -> "does not account" | 17:52:24 |
| 7 Sep 2018 |
|  ralph.johnson set a profile picture. | 09:27:03 |
| ralph.johnson | The design of IELE is inspired by LLVM, but it does not actually use LLVM in its implementation, nor is it a copy. Yes, IELE registers are unbounded integers, and LLVM registers are bounded. A significant part of the effort in proving contracts correct is proving that they have no overflow. By making IELE integers be unbounded, we eliminate those bugs and eliminate that work. | 09:27:03 |
| ralph.johnson | We have a project where we are implementing K by translating it to LLVM. So, we expect in the future to have a version of IELE (which is defined by a K semantics, i.e. a K program) that runs on top of LLVM, but it will just be an implementation technique. We'll do the same for KEVM. | 09:29:01 |
| 8 Sep 2018 |
 @gitter_sebastiengllmt:matrix.org | Yes dwight is right. I was referring to the iele assembler | 13:33:32 |
| @gitter_sebastiengllmt:matrix.org | For example, if you make your @init function public in IELE
It will compile correctly but when you try and submit it to the blockchain you get a well-formed error. It's not obvious at all that the cause of the error was.
In my case I figured it how by having to deploy many contracts -- all slowly removing more lines of code until I figured it out | 13:35:36 |
| 10 Sep 2018 |
| @gcolvin:matrix.org | Thanks much, Ralph. Things are slowly becoming more clear. Next step. In IELE the gas costs vary with the size of the operands. Are those costs computed at runtime, based on the number of bits the result of an operation actually requires? Or are they computed earlier, based on the maximum number of bits the operation could require? | 23:14:00 |
| 11 Sep 2018 |
| ralph.johnson | At runtime. | 12:11:30 |
| ralph.johnson | They are computed each time an instruction executes. You can see exactly how it is done by reading the IELE semantics. It is written in K, which will take some getting used to, but it is quite precise. | 12:15:34 |
| 14 Sep 2018 |
 @gitter_gcolvin:matrix.org | Thanks, Ralph. I very much support such precision, but I can’t read K I fear runtime calculation will be too big of a performance hit when code is compiled down to machine registers. | 22:50:43 |
| @gitter_gcolvin:matrix.org | ( I joke that I’m a mechanic, not a mathematician. I believe formal specs need to be paralleled with precise natural language to be useful to most computer progrmmers.) | 22:52:51 |
| 15 Sep 2018 |
| ralph.johnson | To a mechanic, K is just another programming language. A bit unusual syntax, but far from the worst I have seen. When you are looking at the K definitions of IELE, you are looking at the implementation of IELE. And it is much more readable than most VM implementations. | 11:39:12 |
| ralph.johnson | Runtime calculation of gas is what EVM does. I was going to say "what all the blockchain VMs do" but I don't know about any other than EVM. Calculating gas cost is not a big part of the time in KEVM or IELE, and probably not in EVM either. | 11:42:12 |
| @gcolvin:matrix.org | Well, to a mechanic K is very much higher level than assembly and C ;) | 22:56:41 |
| @gcolvin:matrix.org | Anyway, the EVM operations mostly charge fixed amount of gas, and are still in a big overhead in the C++ interpreter. I reduced it a lot by avoiding unnecessary computations per instruction, it can reduced further by pushing the computations to the end of basic blocks, and even further by hoisting computations further up the tree. If gas is gas calculated per instruction then what might compile to a single operation on two registers becomes that operation plus a more expensive sequence of operations to calculate the gas. | 23:07:35 |
| 25 Sep 2018 |
|  colex joined the room. | 07:40:33 |
| 27 Sep 2018 |
|  @locusf:disroot.org joined the room. | 04:24:50 |
| 3 Oct 2018 |
|  grigore.rosu set a profile picture. | 01:47:12 |
| grigore.rosu | Hi Greg: sorry for not answering earlier, somehow this channel slipped ... too many channels and bridges in my slack. Ralph was right on the spot with his answers. We have suffered a lot with doing formal verification of EVM contracts, lots of errors being indeed due to overflows. So in IELE we decided to favor mathematical clarity, and thus easier formal verification, over gas. | 01:47:13 |
| grigore.rosu | That being said, note that a smart contract owner who respects his clients can formally verify their contract and as part of that give a provably correct formula for how much gas the contract requires as a function of symbolic inputs. | 01:49:58 |
| grigore.rosu | so everybody knows at call-time how much gas a transaction takes | 01:50:44 |
| @gcolvin:matrix.org | I'm drowning in channels, Grigore. I must turn most of them off if am to get anything else done :(. Fair enough choice for IELE. I'm working in the EVM/eWasm world of fixed-width, power-of-two registers, of course. And not wanting to slow down compiled code anymore than necessary. | 02:06:34 |
| @gcolvin:matrix.org | Still, if this gas formula could be part of the required output of the validation of a contract going onto the blockchain, then metering goes away, does it not? | 02:12:59 |
| grigore.rosu | Greg: Yes! And that is a very important point, in favor of formal verification. | 15:51:06 |
| @gitter_gcolvin:matrix.org | This is very exciting. Given a formal spec of a VM and program, I got that useful properties of program can be established at validation time. What properties I’m not sure, EVM 615 sets out just a few. I hadn’t considered that constant-time formulas could be created that establish properties of the program at call time, like how much gas it needs. What else? | 20:58:21 |
| 15 Oct 2018 |
|  holybao joined the room. | 02:07:41 |
| 20 Oct 2018 |
|  @rinor.hoxha:matrix.org joined the room. | 10:02:33 |
| 1 Nov 2018 |
|  ranwar joined the room. | 03:14:01 |
| 6 Jan 2019 |
|  Zaki | iqlusion.io joined the room. | 02:23:20 |
