| 12 Jul 2018 |
 @gitter_gcolvin:matrix.org | An observation and a question. First, I still worry that the time for memory operations may be non-deterministic, and that a deterministic allocator will waste either time or space. I’d prefer to just not have a free operator. But it’s possible to write a determistic allocator, so that might suffice. | 13:25:14 |
| @gitter_gcolvin:matrix.org | Next, some op results have more bits than their operands. But that is not the semantics of LLVM integers. This could force extra nmemory allocation and a mod operation when the extra bits are unwanted. | 13:31:57 |
| 21 Aug 2018 |
|  @gitter_bredamatt:matrix.org joined the room. | 21:56:48 |
| @gitter_bredamatt:matrix.org | Hi, I am highly interested in learning more about IELE and VMs for blockchain technology. I am a fast learner, and currently enrolled in a 4 year PhD program in Informatics. However, I have little experience with VMs. My work is primarily in formal modelling, which also is maths-heavy and semantics oriented. I wanted to ask if there are any good resources available to read so I can up my understanding of VMs before I start looking into writing Smart contracts for the Cardano / Ethereum platform. Best wishes, M | 21:56:57 |
| 24 Aug 2018 |
|  @gitter_sebastiengllmt:matrix.org joined the room. | 07:16:27 |
| @gitter_sebastiengllmt:matrix.org | I don't understand why in https://github.com/runtimeverification/iele-semantics/blob/master/iele-gas.md
he size of the result register REG for an arithmetic operation log2 is set as the constant 2
rule #memory [ REG = log2 W ] => #registerDelta(REG, 2) | 07:16:32 |
| @gitter_sebastiengllmt:matrix.org | I would assume that it is
rule #memory [ REG = log2 W ] => #registerDelta(REG, bitsInWords((bitsInWords(W))
ex: W is 2^64
then log2(W) = bitsInWords(2^64) = 64
and to represent 64=2^6 we need log2(2^6) = bitsInWords(2^6) = 6 bits | 07:20:31 |
| @gitter_sebastiengllmt:matrix.org | (edited) ... that it is ... => ... that the correct version is ... | 07:20:52 |
| @gitter_sebastiengllmt:matrix.org | okay thinking about it I now realize bitsInWords doesn't count #bits as I thought but my confusion about why the constant 2 is used still stands | 07:50:54 |
 dwight.guth | This rule is setting the estimated size of the result of the operation in words. If we assume that the size in bytes of the operand cannot exceed 2^64 (because that's the size of the address space of a modern machine) then the size in bits of the operand cannot exceed 2^67 (ie 2^64 * 8). Since the log base 2 of an positive integer is always equal to the size in bits of an integer minus 1, then the log base 2 of the operand cannot exceed 2^67 - 1, which is less than 2^127-1, the maximum value of a 2 word register | 14:17:26 |
| dwight.guth | In practice it's highly unlikely that the result will ever exceed 1 word, so the second word will probably apply automatically to the cost of the next memory increase, but that's the logic | 14:19:21 |
| 30 Aug 2018 |
|  @rinor.hoxha:matrix.org left the room. | 19:00:19 |
| 4 Sep 2018 |
| @gitter_sebastiengllmt:matrix.org | reminder: rename this channel to something other than "semantics" to encourage more people to join | 04:31:58 |
 @gitter_grosu:matrix.org | @SebastienGllmt They do not seem to allow you to rename a Gitter room; the name is given by the name of the Github repo. And it would be too complicated to rename the Github repo, because we have the convention that all language semantics are suffixed with -semantics. I did change the title of the channel to IELE Virtual Machine for the Blockchain, to be the same as the one in Matrix https://riot.im/app/#/room/#IELE:matrix.org. I hope this is good enough for now. | 22:31:34 |
| 6 Sep 2018 |
| @gitter_sebastiengllmt:matrix.org | Would love if the compiler displayed well-formed errors and gave messages saying which rule is violated. Does anybody have any hint about how to implement that?
I tried compiling the Remix fork myself but it fails to connect to the compiler :( | 05:42:08 |
|  ralph.johnson joined the room. | 15:40:33 |
| ralph.johnson | The Solidity compiler? | 15:40:39 |
| dwight.guth | I think he's referring to the iele assembler | 15:56:04 |
| dwight.guth | specifically, making it so that the contract fails to assemble if the contract is not well-formed, and reports why it's not well formed | 15:56:20 |
 @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 |
