- Join over
**1.5M+ people** - Join over
**100K+ communities** - Free
**without limits** - Create
**your own community**

- Oct 21 04:40charlotte-Zch opened #174
- Sep 30 19:48dwightguth closed #134
- Sep 30 19:48dwightguth closed #96
- Sep 30 19:48dwightguth closed #95
- Sep 30 19:48dwightguth closed #93
- Sep 30 19:46dwightguth closed #66
- Feb 11 16:43
dwightguth on jenkinsfile-dockerfile

- Feb 11 16:43
dwightguth on master

Switch CI over to Jenkinsfile (… (compare)

- Feb 11 16:43dwightguth closed #173
- Feb 09 20:00ehildenb review_requested #173
- Feb 08 20:55dwightguth synchronize #173
- Feb 08 20:55
dwightguth on jenkinsfile-dockerfile

use bash in jenkinsfile so we h… (compare)

- Feb 08 19:59dwightguth synchronize #173
- Feb 08 19:59
dwightguth on jenkinsfile-dockerfile

add netcat dependency (compare)

- Feb 08 19:00dwightguth synchronize #173
- Feb 08 19:00
dwightguth on jenkinsfile-dockerfile

Revert "Makefile: build and ins… Revert "Jenkinsfile: export LD_… install secp256k on bionic via … (compare)

- Feb 07 22:38ehildenb synchronize #173
- Feb 07 22:38
ehildenb on jenkinsfile-dockerfile

Jenkinsfile: export LD_LIBRARY_… (compare)

- Feb 07 21:32ehildenb synchronize #173
- Feb 07 21:32
ehildenb on jenkinsfile-dockerfile

Dockerfile: cache haskell depen… (compare)

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 :).

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 :).

`dwight.guth`

Hi. I was one of the developers behind IELE. Thanks for your suggestions. We are definitely aware that the gas model is a work in progress, so thank you for your offered expertise. I was wondering if you could answer a few questions to help me understand your feedback better.

First, you mention a function of the form y=a+b/(c+x) for memory usage. Can you tell me how you came up with that equation, what each of the constants might signify, and approximately the order of magnitude you had in mind for the constants?

Second, you mention the gas cost for resizing memory. Can you explain in a little bit more detail what the vulnerability you mention is and how you would personally think to alter the gas model of IELE to address these concerns.

The function is just from playing around in a graphing calculator. You can adjust the constants to approximately fit the shape of the function to shape of actual memory performance, and the brick wall of the current physical limit on RAM. Other formulas might do, including some form of exponential. But a quadratic doesn't rise fast enough.

In general, memory management is difficult. The only ones I know of that operate in constant time allocate and free objects of fixed size (typically powers of two) with no attempt to coalesce objects; deallocated objects are simply placed on the free list for their size. Depending on the pattern of access this kind of allocator can waste an arbitrary amount of memory. IELEs variable-sized integers would need to be allocated inside one of these, and would need to be copied and reallocated whenever they filled on up. When that happened would depend on the implementation.

Most memory managers attempt to balance memory usage and speed of allocation with a bag of tricks, none of which is guaranteed to work. The attacks are to find a way to cause the memory manager to use too much RAM and/or too much time relative to the gas spent. The details of an attack vary with the (often quite complex) details of the runtime.

a good starting point for a gas formula that has y=0 when x=0 and asymptotes on 1

A few years old, but not too different. No smooth function is right here. The YP is linear to 724B, which fits no particular hardware boundary, then goes quadratic, which maybe fits through the layers of cache. But it then takes an exponential or steeper to catch the 50:1 increase to RAM. But it's not the cost of allocation that really increases so much as the latency, and that goes up (in the EVM) by the address loaded or stored from. Since the cost for these is set at very-low we might assume that memory access is not intended to be outside of cache.

Some other constraint is needed in the calculation to keep x below 4. Probably suffices to say that if y <= 0 then OOG.

Summary of all the above being

- memory management might too complex for the VM runtime
- the gas function for memory should and can be simple

And of course subtract 1 from these if you to start at zero. At some point this needs to turn into an EIP you can pick up i you want. Currently Ethereum puts such a low limit on memory (less than 32K) that it’s not a DoS vulnerability—you can't get out of the megabytes of cache.

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.

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

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

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)`

`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
`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
@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.
`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
`@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.

`@gcolvin:matrix.org`

"does account" -> "does not account"
`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.
`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.
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

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

`@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?
`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.
( 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.)

`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.
`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.
`@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.
`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.
`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.
`grigore.rosu`

so everybody knows at call-time how much gas a transaction takes
`@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.
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?