rv-jenkins on _update-deps_kframework_k
deps/k_release: v5.1.20 (compare)
rv-jenkins on _update-deps_kframework_k
deps/k_release: v5.1.19 (compare)
ttuegel on release-nix
Build Nix packages in release m… (compare)
rv-jenkins on _update-deps_kframework_k
deps/k_release: v5.1.17 (compare)
dependabot[bot] on npm_and_yarn
Bump lodash from 4.17.19 to 4.1… (compare)
rv-jenkins on _update-deps_kframework_k
deps/k_release: v5.1.16 (compare)
rv-jenkins on gh-pages
Update dependency: deps/k_relea… gh-pages: Updated the website Merge remote-tracking branch 'o… (compare)
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
-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?@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.
@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.
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.
everett.hildenbrandt
test
everett.hildenbrandt
<@U980VHYGY> looks like th ebridge is working
everett.hildenbrandt
Element Bridge: https://app.element.io/#/room/!LtQJkJbwuhxaMuWVOa:matrix.org
everett.hildenbrandt
I can't hear you <@U980VHYGY>!
everett.hildenbrandt
Type louder!
everett.hildenbrandt
test