!MfVXcmpKuyudZHcqil:matrix.org

The K Framework User Group

308 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
16 Jan 2024
@palinatolmach:matrix.orgpalinatolmach
In reply to @xvwx:matrix.dapp.org.uk
Is there a way to tell kontrol to start with a fully abstract storage?
*

We have a cheatcode for that, but it's contract-specific. You can install cheatcodes as a forge library in your project:

forge install runtimeverification/kontrol-cheatcodes

and then use it as follows:

    function testSymbolicStorage(uint256 slot) public {
         address addr = 0xEA674fdDe714fd979de3EdF0F56AA9716B898ec8;
         kevm.symbolicStorage(addr);
         // the storage for addr is symbolic
         // ...
    }
11:22:47
@palinatolmach:matrix.orgpalinatolmach dxo: looks like we'll need a bit more time to agree on the exit code convention, but the counterexample generation fix is ready, and we just have to wait a bit for the PR to go through — I'll send you a message tomorrow once it's published! 15:29:52
@xvwx:matrix.dapp.org.ukdxoawesome15:48:21
@xvwx:matrix.dapp.org.ukdxothanks a lot <315:48:23
@xvwx:matrix.dapp.org.ukdxo
In reply to @palinatolmach:matrix.org

We have a cheatcode for that, but it's contract-specific. You can install cheatcodes as a forge library in your project:

forge install runtimeverification/kontrol-cheatcodes

and then use it as follows:

    function testSymbolicStorage(uint256 slot) public {
         address addr = 0xEA674fdDe714fd979de3EdF0F56AA9716B898ec8;
         kevm.symbolicStorage(addr);
         // the storage for addr is symbolic
         // ...
    }
I see
15:48:27
@xvwx:matrix.dapp.org.ukdxothere are a few benchmarks that check modelling of symbolic storage that expect all storage to be completely abstract at the start15:48:46
@xvwx:matrix.dapp.org.ukdxo both halmos and hevm can be run from the cli like that 15:48:56
@xvwx:matrix.dapp.org.ukdxo I can exclude kontrol from those 15:49:02
@xvwx:matrix.dapp.org.ukdxoit's not a big chunk of cases and I'm sorta considering removing that category entirely15:49:14
17 Jan 2024
@palinatolmach:matrix.orgpalinatolmach Thank you too! We're now generating counterexamples by default, starting with version 0.1.118 :) 05:56:50
@palinatolmach:matrix.orgpalinatolmach
In reply to @xvwx:matrix.dapp.org.uk
there are a few benchmarks that check modelling of symbolic storage that expect all storage to be completely abstract at the start
Oh, I see! I guess, in Kontrol, we can make the storage of all involved contracts symbolic in the setUp or in the test itself, but I agree that it's not exactly the same, and executing kevm.symbolicStorage() cheatcodes would also make it slower (than not having to execute them).
06:11:41
@palinatolmach:matrix.orgpalinatolmachLet me check with the team on the options we might have for enabling all storage to be fully abstract!06:12:08
18 Jan 2024
@palinatolmach:matrix.orgpalinatolmach I filed an issue on --symbolic-storage CLI argument (and exit codes too) — we've discussed both of them internally, and both are certainly feasible, but will take us some time to triage and implement. I'll let you know once that happens, and please let me know if you're having any issues or if anything is unclear too! 08:17:43
19 Jan 2024
@xvwx:matrix.dapp.org.ukdxosweet14:57:32
@xvwx:matrix.dapp.org.ukdxoI'll exclude control from those benchmarks for now14:57:38
@xvwx:matrix.dapp.org.ukdxo does kontrol treat all reverts as failing tests? 15:08:15
@xvwx:matrix.dapp.org.ukdxo both hevm and halmos treat only assertion failures as test failures (i.e. a call to assert or a ds-test assertion violation). 15:09:12
@xvwx:matrix.dapp.org.ukdxo and don't treat reverts from e.g. a call to require as a failing test 15:09:28
@xvwx:matrix.dapp.org.ukdxootherwise you just get a lot of noise relating to e.g. overflow checks15:09:48
@xvwx:matrix.dapp.org.ukdxo and it's pretty convenient to be able to use require as a kind of assume 15:10:04
22 Jan 2024
@palinatolmach:matrix.orgpalinatolmachThanks!15:35:20
@palinatolmach:matrix.orgpalinatolmach Yeah, kontrol reports anything Foundry would report as failure 15:35:35
@xvwx:matrix.dapp.org.ukdxo would there be a way to make kontrol only look for reverts that come from assert and ds-test assertion violations? 20:40:56
23 Jan 2024
@_slack_runtimeverification_U0269R7CNNB:matrix.orgraoul.schaffranek Yeah, sounds like a good idea. We can maybe have different success predicates, e.g. foundry_success, hevm_success for compatibility with different tools. I'll open an issue and keep you updated 12:40:22
@_slack_runtimeverification_U0269R7CNNB:matrix.orgraoul.schaffranek Here is the issue, it's on top of our agenda 🙂 https://github.com/runtimeverification/kontrol/issues/312 13:43:00
11 Feb 2024
@leopoldoezequielriosgonzalez:matrix.org@leopoldoezequielriosgonzalez:matrix.org joined the room.16:28:38
@leopoldoezequielriosgonzalez:matrix.org@leopoldoezequielriosgonzalez:matrix.org left the room.16:28:59
15 Feb 2024
@leopoldoezequielriosgonzalez:matrix.org@leopoldoezequielriosgonzalez:matrix.org joined the room.03:39:49
@leopoldoezequielriosgonzalez:matrix.org@leopoldoezequielriosgonzalez:matrix.org left the room.03:52:43
17 Feb 2024
@monkey:tomesh.net@monkey:tomesh.net left the room.08:54:56

There are no newer messages yet.


Back to Room ListRoom Version: