!MfVXcmpKuyudZHcqil:matrix.org

The K Framework User Group

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

Load older messages


Timestamp Message
7 Feb 2019
18:28:00@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth an alias even if you want
18:28:09@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt a macro was the next thing I was going to try for
18:28:52@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth my advice would be to have one production per complete opcode and use a rule like rule i32.extend_i64 => extend(i32, i64) [alias]
18:29:05@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth and then you just write extend(i32, 64) in the rules in the semantics
18:29:28@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth that way the underscore is never a terminal in the grammar and you also get correct rules regarding layout
18:30:04@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt That's basically what we do now, but then we can't take advantage of two different pieces of common machinery used throughout the sematics (1) rules which unfold folded WASM into unfolded WASM, and (2) rules which type-check the arguments.
18:31:05@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt I think I can figure out a middle ground though, will take some tinkering.
18:31:38@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth hmmm?
18:31:55@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth sorry I don't understand how this approach is any different from what you're asking for except in syntax
18:32:09@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth it should be doable with exactly one extra rule per opcode and no other changes in the complexity of the semantics
18:33:02@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt We have common machinery which loads, typechecks, and unfolds opcodes (all wasm specific things). That machinery depends on things being in the general form of "(" TARGET_TYPE "." OPCODE_NAME ")"
18:33:24@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth ah
18:33:33@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth well
18:33:40@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth in that case
18:33:51@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth you can just make the OPCODE_NAME be syntax OpCode ::= "extend_i64"
18:34:06@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth the exact same process applies it's just that the alias only has one argument instead of two
18:35:36@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt It almost works, but not quite (was my first attempt). Actually because of another issue in the type-checking which I need to discuss with FTN1UV4H before moving forward with a fix.
18:36:17@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth well, regardless, it sounds like you have a path forward and you shouldn't really need "_" to be a terminal in your grammar
18:36:46@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth I agree that being able to support this would be good, but it's not going to happen anytime soon and your grammar will also be more accurate if you do it this way
13 Feb 2019
09:18:54@tkazana-eth:matrix.orgtkazana-eth joined the room.
14 Feb 2019
12:45:35@_slack_runtimeverification_U5FNFKKC5:matrix.orggrigore.rosu @room Question for people interested in K. Any ideas what we can all do to make this happen? https://ethereum-magicians.org/t/jello-paper-as-canonical-evm-spec/2389 Basically to make KEVM into the cannonical EVM specification.
14:15:12@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt I think just continue to maintain KEVM and keep it up to date. There isn't someone who feels they have the authority to "make the switch", but since no one is really putting time into the yellow paper, and we're putting time into KEVM, I think it will be maintained for longer
14:32:14@_slack_runtimeverification_U5FNFKKC5:matrix.orggrigore.rosu I think allowing an alternative syntax for configurations, something like in eDSL (e.g., k: stuff instead of k stuff /k ) can also help. And also when we get a chance to resurrect the Latex generator. All language frameworks have something similar: OTT, Spoofax.
14:39:50@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt We can make a to-do for the latex generator. I think it would take about 2 days to have an MVP, and another week to polish.
14:40:02@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt I don't have the bandwidth at the moment, but can add it to my list.
14:52:48@_slack_runtimeverification_U5FNFKKC5:matrix.orggrigore.rosu 8T2RJ802 thanks! WRT latex generator, we had two different styles: one with bubbles and one with angle barackets. We can start by revising those. The one with bubbles can be seen in this paper: http://fsl.cs.illinois.edu/FSL/papers/2013/rosu-serbanuta-2013-k/rosu-serbanuta-2013-k-public.pdf. The one with angle brackets is, for example, here: http://fsl.cs.illinois.edu/FSL/papers/2015/hathhorn-ellison-rosu-2015-pldi/hathhorn-ellison-rosu-2015-pldi-public.pdf. There were people who really hated the bubble notation and people who loved it, and people who really hated the angle notation and people who really liked it. I believe 7XNEMJHL implemented his own style, in the spirit of the angle notation; can you show us, 7XNEMJHL? 5FRLGXJ9 came up with a nice idea, to have a k.sty file with macros for all the K cells and constructs, and then get one or the other style by simply importing some different macro file (but the K latex generator was independent and unique). Anyway, we should probably discuss the details in other channels. Any other ideas what we can do to increase adoption?
15:02:35@_slack_runtimeverification_U7XNEMJHL:matrix.orgdenis.bogdanas My style was angle brackets, but I extended it to support long rules. I extended k.sty so that brackets could have upt to 5 lines I think, and added a lot of line wraps.
15:03:49@_slack_runtimeverification_U5FNFKKC5:matrix.orggrigore.rosu 7XNEMJHL can you send us a link to your PDF showing your notation at work? I think your PhD thesis?
15:05:27@_slack_runtimeverification_U7XNEMJHL:matrix.orgdenis.bogdanas Look at the appendix: https://fmse.info.uaic.ro/publication/a-complete-semantics-of-java/
15:09:06@_slack_runtimeverification_U5FNFKKC5:matrix.orggrigore.rosu 7XNEMJHL impressive that you managed to fit the entire configuration of Java on less than one page (page 116). Are you OK if I put a link to your thesis on the web, where people discuss the K notation?

Show newer messages


Back to Room List