!MfVXcmpKuyudZHcqil:matrix.org

The K Framework User Group

279 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
13 May 2022
@koding:matrix.orgkoding Is it as in this case, the accounts don't matter as all executions end up in revert. And as there are no accounts the evm visualisation fails? 14:48:38
@koding:matrix.orgkoding * (The value _31 is there in all branches without change.) Is it as in this case, the accounts don't matter as all executions end up in revert. And as there are no accounts the evm visualisation fails? 14:49:31
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt Right, so I think I disabled generating the accounts cells because I wanted to minimize how much state was being mentioned, and those paths do end in revert. 17:04:13
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt But I guess disabling that breaks some assuptions about KLab's visualization. 17:04:25
@koding:matrix.orgkodingI found that it breaks finding the name of the contract that is being debugged. :-) EVM and Stack work (for example, when I hardcode contract name in evmv.js).17:10:46
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt Which version of KLab are you using? 17:14:47
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt If you have a patch that makes it work correctly, or lets the user usppyl contract name on command-line, then I'm sure we can get it merged. 17:15:07
@koding:matrix.orgkodingv0.4.0, commit f22656017:16:02
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt Yeah but which repo? 17:20:04
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt There are several forks. 17:20:07
@koding:matrix.orgkodingGood point. https://github.com/dapphub/klab I will have a closer look on Tuesday or Wednesday and see what patch I can come up with.17:41:02
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt There is a makerdao/klab fork which I think is more up to date. 17:41:59
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt You might try that one. 17:42:06
16 May 2022
@usatokenshash:matrix.org@usatokenshash:matrix.org joined the room.10:19:28
@idahotokens:matrix.org@idahotokens:matrix.org joined the room.11:16:38
@_slack_runtimeverification_U0231EMRYF6:matrix.orgmax.kopinsky in the Haskell backend, we had a script which used to collect kore files from kprove commands using --save-temps. It seems like that's no longer supported, is there an alternative? 16:07:52
@_slack_runtimeverification_U0231EMRYF6:matrix.orgmax.kopinsky I'm not clear on if --save-proof-definition-to is what I want 16:08:23
@_slack_runtimeverification_U0231EMRYF6:matrix.orgmax.kopinsky its help text says "binary version" and not "kore version" so I do not think it is 16:08:52
@_slack_runtimeverification_U9HTHFUBS:matrix.orgradu.mereuta Can you be more clear about your use case? I'm not sure I understand what you are trying to do. But kprove/kprovex should have the option --save-temps which doesn't delete the temp files from the .kprove-xxx directory. You may also want to try --debug to get more information. 16:11:25
@_slack_runtimeverification_U0231EMRYF6:matrix.orgmax.kopinsky They do not have that option. 16:13:57
@_slack_runtimeverification_U0231EMRYF6:matrix.orgmax.kopinsky They used to, but they don't now. 16:14:03
@_slack_runtimeverification_U0231EMRYF6:matrix.orgmax.kopinsky
$ kprovex --help , grep -e '--save-temps'
$
16:14:43
@_slack_runtimeverification_U0231EMRYF6:matrix.orgmax.kopinsky
[Error] Critical: Only one main parameter allowed but found several:
"tests/specs/examples/sum-to-n-spec.k" and "--save-temps"
(from kprovex as well)
16:15:13
@_slack_runtimeverification_U0231EMRYF6:matrix.orgmax.kopinsky we want to do exactly this, and then we search that directory for definition.kore and vdefinition.kore and save them. That way we can build a script to run the proof again without having to go through the frontend and such. We use this to generate regression tests in the Haskell backend 16:16:06
@_slack_runtimeverification_U0231EMRYF6:matrix.orgmax.kopinsky
$ kprovex --version
K version:    5.3.36
Build date:   Fri May 06 14:46:04 CDT 2022
16:16:36
@_slack_runtimeverification_U9HTHFUBS:matrix.orgradu.mereuta kprovex --debug spec.k should do what you are looking for. It keeps the .kprove-xxx folder in which it stores the spec.kore and result.kore file which are given as input to the haskell backend. vdefinition.kore doesn't exist anymore. We're using the unmodified definition.kore from the kompiled directory. 16:26:15
@idahotokens:matrix.org@idahotokens:matrix.org left the room.16:26:51
@_slack_runtimeverification_U0231EMRYF6:matrix.orgmax.kopinsky I'll give that a shot 16:30:44
@_slack_runtimeverification_U0231EMRYF6:matrix.orgmax.kopinsky OK, I think that's working. Thanks! 16:31:11
@usatokenshash:matrix.org@usatokenshash:matrix.org left the room.21:41:27

There are no newer messages yet.


Back to Room List