| 11 Jan 2021 |
 everett.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 | Ah gotcha, yeah so we should stand up our own mantis client/KEVM on our platform | 16:45:55 |
| everett.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 |
| everett.hildenbrandt | Right. | 16:46:02 |
| jdneidig | oh 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 | let me get this on our next sprints and have my devs join this riot room | 16:47:26 |
| jdneidig | thanks everett.hildenbrandt 👍️ | 16:51:24 |
| everett.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 | No worries, this space is so fast paced | 16:53:06 |
| 13 Jan 2021 |
 xvwx | Hey :) | 13:31:36 |
| xvwx | What is the difference between ==K and ==String/==Bool/==Int? | 13:31:57 |
| xvwx | can they be used interchangeably? | 13:32:20 |
| everett.hildenbrandt | Well, not really. It depends on the backend you are using how each is interpreted. | 13:43:20 |
| everett.hildenbrandt | On the concrete backends, it shouldn't matter, just will mean exact constructor equality | 13:43:45 |
| everett.hildenbrandt | But on the symbolic backends there can be more/less intelligent handling of each different one. | 13:44:03 |
| everett.hildenbrandt | The Java backend will turn all ==Sort into ==K to do unification over (so it loses the sort information) | 13:44:22 |
| everett.hildenbrandt | The Haskell backend will try to specialize all ==K into the more specific ==Sort if there is one available. | 13:44:40 |
| everett.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 | I see! | 14:11:58 |
| xvwx | 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 | Does ==String make sense? | 14:12:59 |
| xvwx | * 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 |
| everett.hildenbrandt | Is ByteString a sort you defined? | 14:19:21 |
| everett.hildenbrandt | Then definitely ==K | 14:19:37 |
| everett.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 | ByteString is the haskell ByteString | 14:25:45 |
| xvwx | any changes to ethereum/act are very welcome | 14:26:06 |
| xvwx | we're not really working on klab atm, so I dunno how much bandwidth we have to review there | 14:26:46 |
| xvwx | but I would be very happy to give you commit access if you're interested in looking after it? | 14:29:32 |
| xvwx | 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 |
