!LtQJkJbwuhxaMuWVOa:matrix.org

IELE Virtual Machine

82 Members
The IELE Virtual Machine for the Blockchain21 Servers

Load older messages


SenderMessageTime
8 May 2018
@gitter_gcolvin:matrix.org@gitter_gcolvin:matrix.org (edited) Oh, a good starting point for a gas formula that has y=0 when x=0 and asymptotes on 1 is => a good starting point for a gas formula that has y=0 when x=0 and asymptotes on 1 00:14:49
@gitter_gcolvin:matrix.org@gitter_gcolvin:matrix.org https://www.extremetech.com/wp-content/uploads/2014/08/latency.png 04:56:42
@gitter_gcolvin:matrix.org@gitter_gcolvin:matrix.org 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 can assume that memory access is not intended to be outside of cache. 05:14:11
@gitter_gcolvin:matrix.org@gitter_gcolvin:matrix.org (edited) ... we can assume that memory access is not intended to be outside of cache. => ... we might assume that memory access is not intended to be outside of cache. 05:17:58
@gitter_gcolvin:matrix.org@gitter_gcolvin:matrix.org Regardless, we'd like for the cost of memory allocation to approach a brick wall at whatever the maximum reasonable memory allowed to a contract is. 05:19:14
11 May 2018
@gitter_gcolvin:matrix.org@gitter_gcolvin:matrix.org And if I haven’t prattled on enough (and I hope you are reading this on Gitter, not on Riot, where my every edit is preserved) I’ll note that y = 2 ^ x gives a very similar curve. 03:44:07
@gitter_gcolvin:matrix.org@gitter_gcolvin:matrix.org 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
03:44:18
19 May 2018
@rinor.hoxha:matrix.org@rinor.hoxha:matrix.org joined the room.10:03:25
26 Jun 2018
@gitter_gcolvin:matrix.org@gitter_gcolvin:matrix.org 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. 16:46:03
@gitter_gcolvin:matrix.org@gitter_gcolvin:matrix.orgWhat I’m up to is slowly critiquing my way through this beautiful work as a means of understanding it. I’m a volunteer Etherian at this point, so it’s very slow.16:51:55
2 Jul 2018
@pox:matrix.orgpox joined the room.01:11:47
12 Jul 2018
@gitter_gcolvin:matrix.org@gitter_gcolvin:matrix.orgAn 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@gitter_gcolvin:matrix.orgNext, 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@gitter_bredamatt:matrix.org joined the room.21:56:48
@gitter_bredamatt:matrix.org@gitter_bredamatt:matrix.orgHi, 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, M21:56:57
24 Aug 2018
@gitter_sebastiengllmt:matrix.org@gitter_sebastiengllmt:matrix.org joined the room.07:16:27
@gitter_sebastiengllmt:matrix.org@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@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@gitter_sebastiengllmt:matrix.org (edited) ... that it is ... => ... that the correct version is ... 07:20:52
@gitter_sebastiengllmt:matrix.org@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
@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.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
@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.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@rinor.hoxha:matrix.org left the room.19:00:19
4 Sep 2018
@gitter_sebastiengllmt:matrix.org@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@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@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
@_slack_runtimeverification_U8U8CMMV2:matrix.orgralph.johnson joined the room.15:40:33
@_slack_runtimeverification_U8U8CMMV2:matrix.orgralph.johnson The Solidity compiler? 15:40:39
@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth I think he's referring to the iele assembler 15:56:04
@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.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

Show newer messages


Back to Room ListRoom Version: