!MfVXcmpKuyudZHcqil:matrix.org

The K Framework User Group

228 Members
The K Framework (kframework.org) and its applications to smart contracts.  EVM: github.com/kframework/evm-semantics Viper: github.com/kframework/viper-semantics46 Servers

Load older messages


SenderMessageTime
11 Jan 2021
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt Well, you would be having SIMBA talk to the Mantis client, specifically. And then KEVM lives under the Mantis client. 16:45:15
@jdneidig:matrix.orgjdneidigAh gotcha, yeah so we should stand up our own mantis client/KEVM on our platform 16:45:55
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt I'm not sure what the status of the KEVM - Mantis integration is at the moment though. But either way, KEVM is just the VM implementation, and Mantis is the client that you would be deploying to (which will handle talking to KEVM properly). 16:45:59
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt Right. 16:46:02
@jdneidig:matrix.orgjdneidigoh ok, yeah we can help, we open sourced some of the Hyperledger EVM fixes and implementation for python, so we are happy to contribute to community to get it going 16:46:50
@jdneidig:matrix.orgjdneidiglet me get this on our next sprints and have my devs join this riot room16:47:26
@jdneidig:matrix.orgjdneidig thanks everett.hildenbrandt 👍️ 16:51:24
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt Yep, happy to help. I'll also investigate the current status of the Mantis - KEVM integration, so next time you ask I have a better answer for you. 16:52:09
@jdneidig:matrix.orgjdneidigNo worries, this space is so fast paced 16:53:06
13 Jan 2021
@xvwx:matrix.dapp.org.ukxvwxHey :)13:31:36
@xvwx:matrix.dapp.org.ukxvwx What is the difference between ==K and ==String/==Bool/==Int? 13:31:57
@xvwx:matrix.dapp.org.ukxvwxcan they be used interchangeably?13:32:20
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt Well, not really. It depends on the backend you are using how each is interpreted. 13:43:20
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt On the concrete backends, it shouldn't matter, just will mean exact constructor equality 13:43:45
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt But on the symbolic backends there can be more/less intelligent handling of each different one. 13:44:03
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt The Java backend will turn all ==Sort into ==K to do unification over (so it loses the sort information) 13:44:22
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt The Haskell backend will try to specialize all ==K into the more specific ==Sort if there is one available. 13:44:40
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt So when you write lemmas for the symbolic backends, if you are writing one like this for the Java backend:
rule I ==K I +Int J => J ==Int 0 [simplification]
would need to be changed to this for the Haskell backend:
rule I ==Int I +Int J => J ==Int 0 [simplification]
13:45:37
@xvwx:matrix.dapp.org.ukxvwxI see!14:11:58
@xvwx:matrix.dapp.org.ukxvwx I'm making some tweaks to the K backend for act, and I'm wondering which is the best equality operator to use for ByteString types (bytes and string abi types are represented as ByteString in the act AST). 14:12:54
@xvwx:matrix.dapp.org.ukxvwx Does ==String make sense? 14:12:59
@xvwx:matrix.dapp.org.ukxvwx * I'm making some tweaks to the K backend for act, and I'm wondering which is the best equality operator to use for ByteString types (bytes and string abi types are represented as ByteString in the act AST). 14:13:13
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt Is ByteString a sort you defined? 14:19:21
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt Then definitely ==K 14:19:37
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt Also, I have some significant changes to the generation of K from ACT, and some other changes to KLab as well. Is there any interest in upstreaming these? 14:20:19
@xvwx:matrix.dapp.org.ukxvwx ByteString is the haskell ByteString 14:25:45
@xvwx:matrix.dapp.org.ukxvwx any changes to ethereum/act are very welcome 14:26:06
@xvwx:matrix.dapp.org.ukxvwx we're not really working on klab atm, so I dunno how much bandwidth we have to review there 14:26:46
@xvwx:matrix.dapp.org.ukxvwxbut I would be very happy to give you commit access if you're interested in looking after it?14:29:32
@xvwx:matrix.dapp.org.ukxvwx
In reply to @_slack_runtimeverification_U8T2RJ802:matrix.org
Also, I have some significant changes to the generation of K from ACT, and some other changes to KLab as well. Is there any interest in upstreaming these?
* any changes to ethereum/act are very welcome
14:32:46

There are no newer messages yet.


Back to Room List