| 16 Jan 2024 |
 dxo | 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 |
| dxo | there are a few benchmarks that check modelling of symbolic storage that expect all storage to be completely abstract at the start | 15:48:46 |
| dxo | both halmos and hevm can be run from the cli like that | 15:48:56 |
| dxo | I can exclude kontrol from those | 15:49:02 |
| dxo | it's not a big chunk of cases and I'm sorta considering removing that category entirely | 15:49:14 |
| 17 Jan 2024 |
 palinatolmach | Thank you too! We're now generating counterexamples by default, starting with version 0.1.118 :) | 05:56:50 |
| palinatolmach | 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 | Let 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 | 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 |
| dxo | sweet | 14:57:32 |
| dxo | I'll exclude control from those benchmarks for now | 14:57:38 |
| dxo | does kontrol treat all reverts as failing tests? | 15:08:15 |
| dxo | 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 |
| dxo | and don't treat reverts from e.g. a call to require as a failing test | 15:09:28 |
| dxo | otherwise you just get a lot of noise relating to e.g. overflow checks | 15:09:48 |
| dxo | and it's pretty convenient to be able to use require as a kind of assume | 15:10:04 |
| 22 Jan 2024 |
| palinatolmach | Thanks! | 15:35:20 |
| palinatolmach | Yeah, kontrol reports anything Foundry would report as failure | 15:35:35 |
| dxo | 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 |
 raoul.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 |
| raoul.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 joined the room. | 16:28:38 |
| @leopoldoezequielriosgonzalez:matrix.org left the room. | 16:28:59 |
| 15 Feb 2024 |
| @leopoldoezequielriosgonzalez:matrix.org joined the room. | 03:39:49 |
| @leopoldoezequielriosgonzalez:matrix.org left the room. | 03:52:43 |
| 17 Feb 2024 |
|  @monkey:tomesh.net left the room. | 08:54:56 |
| 27 Mar 2024 |
|  David | W3F changed their display name from David | W3F to David | W3F - OOO Apr 02. | 17:08:39 |
| 2 Apr 2024 |
| David | W3F changed their display name from David | W3F - OOO Apr 02 to David | W3F. | 06:59:48 |
| 7 Apr 2024 |
|  mehmetoguzderin changed their profile picture. | 10:12:13 |
| 11 Apr 2024 |
| mehmetoguzderin changed their profile picture. | 11:09:53 |
