|14 Feb 2019|
|15:10:09||denis.bogdanas|| sure |
|19:02:48||dwight.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:31||everett.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:58||everett.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:09||everett.hildenbrandt|| Then we can play with the actual latex that's generated. |
|19:06:21||everett.hildenbrandt|| Another option, of course, being that we can generate HTML instead of LaTeX. |
|19:07:04||everett.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:14||dwight.guth|| That's probably better for the jello paper as well |
|19:07:25||dwight.guth|| HTML I mean |
|19:07:38||everett.hildenbrandt|| Yeah, it's probably true. |
|19:08:25||everett.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:34||everett.hildenbrandt|| (using something like MathJax on the HTML side) |
|19:08:51||everett.hildenbrandt|| But I find it unlikely we can use pure LaTeX math, though maybe the angle-bracket style notation it's possible. |
|19:09:17||everett.hildenbrandt|| Basically want to commit as little as possible to the final format, and let pandoc handle the rest of the conversion. |
|23:16:46||nishantjr|| 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:47||vladimir.ciobanu|| You can just do |
mvn package -Dllvm.backend.skip to skip it.
|15 Feb 2019|
|00:19:07||dwight.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:01||yudetamago joined the room.|
|07:03:57||yudetamago changed their display name from yudetamago_orz to yudetamago.|
|10:24:05||rikard.hjort joined the room.|
|10:24:05||rikard.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 |
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:37||tkazana-eth||More specifically: did you omit functions with dynamic arrays in input because it is very hard to prove their correctness?|
|15:26:23||tkazana-eth||Even in the current git repository, there is a function setupSafe but with hardcoded length of the array equal to 2|
|15:27:02||tkazana-eth||Are my observations correct or I do not see/understand something?|
|17:11:02||denis.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:50||daejun.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:04||daejun.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|
In reply to @_slack_runtimeverification_U5FNFKKC5:matrix.org 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
@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.
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.
|13:54:06||grigore.rosu|| Thanks for your thoughts @equivrel (Lev)! I fully agree, of course. Feel free to add some comments to https://ethereum-magicians.org/t/jello-paper-as-canonical-evm-spec/2389, too, they may help the EF make a decision to fund this effort. |