!MfVXcmpKuyudZHcqil:matrix.org

The K Framework User Group

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

Load older messages


SenderMessageTime
9 Sep 2022
@david:web3.foundationDavid changed their display name from David to David - ooo until Sept 24.20:42:00
13 Sep 2022
@spiceusabtc:matrix.org@spiceusabtc:matrix.org left the room.13:54:11
19 Sep 2022
@enzoevers:matrix.orgEnzo EversThe K summarizer is still in development I think right? (https://www.youtube.com/watch?v=1iaqWUm0BRI). Or is there already something out there which we can try?11:36:02
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt It's closed at the moment, still developing. Stay tuned though! Happy to answer any questions about it. 14:45:07
@indolering:matrix.orgindolering (Old) joined the room.23:33:37
20 Sep 2022
@indolering:matrix.orgindolering (Old) I read a report from a symposium on secure compilation and it seems like a lot of overlap between the issues they are grappling with and the work done with K Framework and IELE. I submitted it to Lobste.rs and the lead author (who works on CHERI, Capsicum, and Verona) popped up in the comments section. I was thinking this would be a good opportunity for cross pollination ... maybe someone from the K/IELE community could answer their questions? 00:13:03
@indolering:matrix.orgindolering (Old)What is IELE's status? It looks like some crypo funding dried up?00:22:02
@stevenkkok:matrix.orgstevenkkokimage.png
Download image.png
03:39:36
@stevenkkok:matrix.orgstevenkkokRedacted or Malformed Event03:39:57
@stevenkkok:matrix.orgstevenkkokimage.png
Download image.png
03:42:32
@stevenkkok:matrix.orgstevenkkokI try to define expression, but this definition doesn't work well for + and -. 03:42:33
@stevenkkok:matrix.orgstevenkkokHow can I solve this problem?03:42:51
@enzoevers:matrix.orgEnzo EversRedacted or Malformed Event06:04:41
@enzoevers:matrix.orgEnzo Evers
In reply to @stevenkkok:matrix.org
How can I solve this problem?
Spaces are required. "x+1" needs to be "x + 1".
06:05:04
@_slack_runtimeverification_U02CDU166EL:matrix.orgbruce.collie This is likely because you're using the INT-SYNTAX module, rather than UNSIGNED-INT-SYNTAX. There's an explanation in the K standard library file: https://kframework.org/k-distribution/include/kframework/builtin/domains/ 06:07:53
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt @Indolering we haven't workend on KIELE for a while now, indeed the project was suspended indefinitely. IELE was our attempt to make a safer VM for blockchain applications, by borrowing a lot of good ideas from LLVM (indeed, we have several LLVM experts on staff to help with this). Happy to answer any questinos we can about it, but I don't foresee development starting up again soon 😢 14:20:23
22 Sep 2022
@enzoevers:matrix.orgEnzo EversI was trying to work with the kevm docker image but got into a problem with paths. I also created an issue (see issue: https://github.com/runtimeverification/evm-semantics/issues/1390) for this since (I think) it has something to to with the container itself. But I though I would also put the question here.06:42:27
@enzoevers:matrix.orgEnzo EversIn this group I saw that there is also a slack channel. I'm very much interested in the k framework and its formal logic behind it. Would it be possible for me to get invited to the slack channel? enzoevers@gmail.com09:59:08
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt @Enzo I will send you an invite. 14:39:39
@enzoevers:matrix.orgEnzo Evers
In reply to @_slack_runtimeverification_U8T2RJ802:matrix.org
@Enzo I will send you an invite.
Thank you!
15:18:35
23 Sep 2022
@babypumpkin:matrix.orgbabypumpk1n changed their display name from babypumpkin to babypumpk1n.01:31:50
26 Sep 2022
@enzoevers:matrix.orgEnzo Evers set a profile picture.03:38:09
@david:web3.foundationDavid changed their display name from David - ooo until Sept 24 to David.06:02:06
2 Oct 2022
@sirinath:matrix.orgsirinath joined the room.18:03:56
4 Oct 2022
@niconaus:matrix.orgniconausI would love to get in on the slack channel as well! niconaus@gmail.com01:14:45
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt Invite sent! 17:09:32
5 Oct 2022
@test5848:matrix.org@test5848:matrix.org joined the room.12:05:59
@test5848:matrix.org@test5848:matrix.org left the room.12:07:34
6 Oct 2022
@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth M [ A ] is sort KItem because maps are not polymorphic in their value sort currently. You need to cast it to a Byte 17:25:47
@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth That being said, have you considered using the builtin Bytes type? It's likely to be much more performant 17:26:26

There are no newer messages yet.


Back to Room List