!LtQJkJbwuhxaMuWVOa:matrix.org

IELE Virtual Machine

35 Members
The IELE Virtual Machine for the Blockchain2 Servers

Load older messages


Timestamp Message
14 Sep 2018
22:52:51@gitter_gcolvin:matrix.orgGreg Colvin (Gitter)( 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.)
15 Sep 2018
11:39:12@_slack_runtimeverification_U8U8CMMV2:matrix.orgralph.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:42:12@_slack_runtimeverification_U8U8CMMV2:matrix.orgralph.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.
22:56:41@gcolvin:matrix.org@gcolvin:matrix.orgWell, to a mechanic K is very much higher level than assembly and C ;)
23:07:35@gcolvin:matrix.org@gcolvin:matrix.orgAnyway, 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.
25 Sep 2018
07:40:33@colex:matrix.orgcolex joined the room.
27 Sep 2018
04:24:50@locusf:disroot.orglocusf joined the room.
3 Oct 2018
01:47:12@_slack_runtimeverification_U5FNFKKC5:matrix.orggrigore.rosu set a profile picture.
01:47:13@_slack_runtimeverification_U5FNFKKC5:matrix.orggrigore.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:49:58@_slack_runtimeverification_U5FNFKKC5:matrix.orggrigore.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:50:44@_slack_runtimeverification_U5FNFKKC5:matrix.orggrigore.rosu so everybody knows at call-time how much gas a transaction takes
02:06:34@gcolvin:matrix.org@gcolvin:matrix.orgI'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:12:59@gcolvin:matrix.org@gcolvin:matrix.orgStill, 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?
15:51:06@_slack_runtimeverification_U5FNFKKC5:matrix.orggrigore.rosu Greg: Yes! And that is a very important point, in favor of formal verification.
20:58:21@gitter_gcolvin:matrix.orgGreg Colvin (Gitter)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?
15 Oct 2018
02:07:41@holybao:matrix.orgholybao joined the room.
20 Oct 2018
10:02:33@rinor.hoxha:matrix.orgrinor joined the room.
1 Nov 2018
03:14:01@ranwar:matrix.orgranwar joined the room.
6 Jan 2019
02:23:20@zmanian:matrix.orgZaki joined the room.
26 Mar 2019
22:02:53@jurajselep:matrix.orgjurajselep | simplestaking.com changed their display name from jurajselep(simplestaking.com) to jurajselep | simplestaking.com.
23 Apr 2019
10:00:15@dima_tr:matrix.orgdima_tr joined the room.
5 May 2019
19:05:55@xp4.2:matrix.orgxp4.2 joined the room.
7 May 2019
12:09:36@rinor.hoxha:matrix.orgrinor left the room.
1 Aug 2019
15:01:24@locusf:disroot.orglocusf changed their profile picture.
15:01:26@slackbot:matrix.orgSlack Integration set their display name to Slack Integration.
12 Aug 2019
12:46:09@locusf:disroot.orglocusf left the room.
20 Aug 2019
13:42:41@gitter_bredamatt:matrix.orgMattia Bradascio (Gitter) changed their display name from Mattia L.V. Bradascio (Gitter) to Mattia Bradascio (Gitter).
25 Aug 2019
02:11:40@micdecipli5:matrix.orgmicdecipli5 joined the room.
02:11:49@micdecipli5:matrix.orgmicdecipli5 left the room.
26 Oct 2019
16:15:18@charlotte_ldmc:matrix.orgcharlotte_ldmc joined the room.

There are no newer messages yet.


Back to Room List