The K Framework User Group

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

Timestamp Message
14 Feb 2019
15:10:09denis.bogdanas sure
19:02:48dwight.guth The problem with the bubbles was that it simply did not scale to large rules, which are common in real semantics. I think we are better off investing in a implementation of the k language in a syntax highlighting tool and then making clever use of pandoc, than to try to reinvest in the latex generation
19:05:31everett.hildenbrandt Well, the latex generation will be the same either way, but we'll use it as a pandoc filter when generating latex from the markdown.
19:05:58everett.hildenbrandt Pandoc supports external programs being called to format the codeblocks, so I imagine I can re-use chunks of kdoc to do the initial latex generation as a filter for pandoc.
19:06:09everett.hildenbrandt Then we can play with the actual latex that's generated.
19:06:21everett.hildenbrandt Another option, of course, being that we can generate HTML instead of LaTeX.
19:07:04everett.hildenbrandt That may be more flexible in the long term. Either way, there is some infrastructure that needs setup, namely, the ability to translate 1 rule at a time after having read the entire definition in.
19:07:14dwight.guth That's probably better for the jello paper as well
19:07:25dwight.guth HTML I mean
19:07:38everett.hildenbrandt Yeah, it's probably true.
19:08:25everett.hildenbrandt Then the third (and probably most robust option) is to generate in a subset of HTML that pandoc handles translating to LaTeX well. For instance, if we generated everything in pure LaTeX math, then Pandoc can convert that to both HTML and to LaTeX.
19:08:34everett.hildenbrandt (using something like MathJax on the HTML side)
19:08:51everett.hildenbrandt But I find it unlikely we can use pure LaTeX math, though maybe the angle-bracket style notation it's possible.
19:09:17everett.hildenbrandt Basically want to commit as little as possible to the final format, and let pandoc handle the rest of the conversion.
23:16:46nishantjr 5GE6G57G Is it possible to build K either without the LLVM backend, or to ask the LLVM backend to use clang++ as the compiler (instead of clang++-6.0, which is not available through my distro)
23:54:47vladimir.ciobanu You can just do mvn package -Dllvm.backend.skip to skip it.
15 Feb 2019
00:19:07dwight.guth yeah I would skip it for now; llvm 7 has a bug in it that breaks the llvm backend and so I am waiting to support arch linux until llvm 8 comes out later this month
07:03:01yudetamago joined the room.
07:03:57yudetamago changed their display name from yudetamago_orz to yudetamago.
10:24:05rikard.hjort joined the room.
10:24:05rikard.hjort 5FNFKKC5 Like 5GE6G57G said, there may be issues using the bubbles to display large rules. But it would be helpful if it was possible to mix them in a single document. For displaying and explaining the configuration, I think the bubbles do a great job, information-hierarchy-wise. It is also generally very helpful when reading a paper to have an alternative, pictorial representation of central concepts, since that's a good way to sanity-check oneself. If I'm just seeing angle brackets in the entire paper, I might wonder if I've really grasped them. I also want to float
15:22:44tkazana-ethHi guys, I have recently started exploring formal verification ecosystem. At some point I started to analyze Gnosis contract that was proved with K. My question is about that proof. I am looking to the .ini file that defines the specification (v. 0.1.0 commit 427d6f7). Am I right that in that version you do not include a spec for setup function?
15:23:37tkazana-ethMore specifically: did you omit functions with dynamic arrays in input because it is very hard to prove their correctness?
15:26:23tkazana-ethEven in the current git repository, there is a function setupSafe but with hardcoded length of the array equal to 2
15:27:02tkazana-ethAre my observations correct or I do not see/understand something?
17:11:02denis.bogdanas We only proved a subset of Gnosis SafeContracts. Setup function was not covered. Dynamic arrays are hard, but within the capabilities of kprove. Soon we will publish the report on Gnosis project that details what part exactly we verified.
19:36:50daejun.park We were asked to verify (the most important) part of their code as our first engagement with Gnosis, and the setup function is not in the scope. We plan to discuss about the next engagement once the first one is wrapped up.
19:43:04daejun.park The dynamic sized array is challenging to verify, but our K verification tool can handle it. Indeed, we have verified the checkSignature function, which involves the dynamic array and is a lot more complicated than the setup function.
18 Feb 2019
12:15:14equivrel
Hi Grigore (this is Lev 👋 ), IMO one of the biggest issues with the yellow paper is that it is kind of unmaintained. Today I was reporting what I believe is an error in it, and noticed that there are dozens of issues and PRs fixing stuff that have been hanging around untriaged for months. I can't say definitively since I don't know who is responsible for it at this point, but you could easily come to the conclusion that it's not really maintained. I wouldn't be surprised if the constantinople changes get added at some point before we go live, even though they haven't been added yet and Constantinople was on the verge of going live last month, but smaller corrections seem to go unfixed. This is in stark contrast to evm-semantics which is of course very actively maintained and where it is easy to get a correction merged. I think for something as crucial as a language specification, this alone is reason enough to prefer the more maintained one, not to mention that IMO it's more precise, readable, etc.