Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Extending CSE support #355

Merged
merged 114 commits into from
Mar 15, 2024
Merged

Extending CSE support #355

merged 114 commits into from
Mar 15, 2024

Conversation

PetarMax
Copy link
Contributor

@PetarMax PetarMax commented Feb 9, 2024 •
edited
Loading

This PR provides infrastructure and tests in order to extend the support we have for CSE. In particular:

  • it adds a number of CSE-related tests into a separate CI job; some are not run because of a bug in the booster that is to be fixed by this PR.
  • To relieve pressure off of the CI, we are running only the CSE versions of the CSE-related tests and commenting out not the non-CSE ones. Eventually, both should be run since they will allow for a precise comparison of the effects of CSE.
  • It adds a file with lemmas useful for CSE. These lemmas may be upstreamable to KEVM in subsequent PRs.

@PetarMax PetarMax added the enhancement New feature or request label Feb 9, 2024
@PetarMax PetarMax self-assigned this Feb 9, 2024
@PetarMax PetarMax mentioned this pull request Feb 9, 2024
Closed
@PetarMax PetarMax linked an issue Feb 9, 2024 that may be closed by this pull request
External calls in CSE executions #356
Closed
@ehildenb
Copy link
Member

ehildenb commented Feb 9, 2024

Make sure to coordinate with @anvacaru , who has some work here: #347.

I think it may be useful to focus on internal functions in parallel to his work on automating CSE.

@PetarMax PetarMax mentioned this pull request Feb 12, 2024
Open
rv-jenkins and others added 7 commits February 13, 2024 12:31
@rv-jenkins @PetarMax
Update dependency: deps/kevm_release (#364)
b0d2270 
* deps/kevm_release: Set Version 1.0.452

* Set Version: 0.1.155

* Sync Poetry files: kevm-pyk version 1.0.452

* flake.{nix,lock}: update Nix derivations

* Sync Poetry files: kevm-pyk version 1.0.452

* Sync Poetry files: kevm-pyk version 1.0.452

* Sync Poetry files: kevm-pyk version 1.0.452

* Sync Poetry files: kevm-pyk version 1.0.452

* Sync Poetry files: kevm-pyk version 1.0.452

* Sync Poetry files: kevm-pyk version 1.0.452

---------

Co-authored-by: devops <[email protected]>
Set Version: 0.1.156
5e7808d
@PetarMax
merge with master
611d972
Set Version: 0.1.158
2eb00d3
@PetarMax
Merge branch 'master' into petar/cse-exploration
0cf45fd
Set Version: 0.1.167
f65a253
@PetarMax
refactoring, removing unneeded files
8420897
@PetarMax PetarMax changed the title Extending CSE support Extending CSE support: External Function Calls Feb 22, 2024
PetarMax and others added 7 commits February 22, 2024 17:35
@PetarMax
Merge branch 'master' into petar/cse-exploration
e9dd9c3
Set Version: 0.1.169
b8209ee
@lucasmt @PetarMax
Add kontrol refute-node and kontrol unrefute-node commands (#381)
fca77f7 
* Implement kontrol refute-node command

* Implement kontrol unrefute-node command

* Filter proof versions to exclude subproofs

* Factor out foundry_refute_node and foundry_unrefute_node

* Add test for foundry_refute_node

* Add expected output for node refutation test

* Set Version: 0.1.165

* Set Version: 0.1.169

---------

Co-authored-by: Lucas MT <[email protected]>
Co-authored-by: devops <[email protected]>
@rv-jenkins @palinatolmach @PetarMax
Update dependency: deps/kevm_release (#392)
c8d6329 
* deps/kevm_release: Set Version 1.0.462

* Set Version: 0.1.169

* Sync Poetry files: kevm-pyk version 1.0.462

* flake.{nix,lock}: update Nix derivations

* Set Version: 0.1.170

* flake.{nix,lock}: update Nix derivations

* deps/kevm_release: Set Version 1.0.463

* Sync Poetry files: kevm-pyk version 1.0.463

* flake.{nix,lock}: update Nix derivations

* Updated expected output

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Palina Tolmach <[email protected]>
Set Version: 0.1.171
8bcbf47
@PetarMax
merge with master
4850100
Set Version: 0.1.172
f798d5e
@PetarMax
Copy link
Contributor Author

There is an adjustment that needs to be made, please don't merge this PR until the following commit.

@PetarMax PetarMax changed the title Extending CSE support [DO-NOT-MERGE] Extending CSE support Mar 14, 2024
@PetarMax PetarMax changed the title [DO-NOT-MERGE] Extending CSE support Extending CSE support Mar 14, 2024
This was referenced Mar 15, 2024
Merged
Merged
Merged
@rv-jenkins rv-jenkins merged commit 8c41d6f into master Mar 15, 2024
12 checks passed
@rv-jenkins rv-jenkins deleted the petar/cse-exploration branch March 15, 2024 18:41
qian-hu pushed a commit that referenced this pull request Mar 18, 2024
@PetarMax @rv-jenkins
@lucasmt @palinatolmach @ehildenb @anvacaru @lisandrasilva @tothtamas28 @qian-hu
Extending CSE support (#355)
01cbbef 
* test for CSE function calls

* Set Version: 0.1.152

* Set Version: 0.1.153

* further examples, tests, and lemmas

* Set Version: 0.1.155

* Update dependency: deps/kevm_release (#364)

* deps/kevm_release: Set Version 1.0.452

* Set Version: 0.1.155

* Sync Poetry files: kevm-pyk version 1.0.452

* flake.{nix,lock}: update Nix derivations

* Sync Poetry files: kevm-pyk version 1.0.452

* Sync Poetry files: kevm-pyk version 1.0.452

* Sync Poetry files: kevm-pyk version 1.0.452

* Sync Poetry files: kevm-pyk version 1.0.452

* Sync Poetry files: kevm-pyk version 1.0.452

* Sync Poetry files: kevm-pyk version 1.0.452

---------

Co-authored-by: devops <[email protected]>

* Set Version: 0.1.156

* Set Version: 0.1.158

* Set Version: 0.1.167

* refactoring, removing unneeded files

* Set Version: 0.1.169

* Add `kontrol refute-node` and `kontrol unrefute-node` commands (#381)

* Implement kontrol refute-node command

* Implement kontrol unrefute-node command

* Filter proof versions to exclude subproofs

* Factor out foundry_refute_node and foundry_unrefute_node

* Add test for foundry_refute_node

* Add expected output for node refutation test

* Set Version: 0.1.165

* Set Version: 0.1.169

---------

Co-authored-by: Lucas MT <[email protected]>
Co-authored-by: devops <[email protected]>

* Update dependency: deps/kevm_release (#392)

* deps/kevm_release: Set Version 1.0.462

* Set Version: 0.1.169

* Sync Poetry files: kevm-pyk version 1.0.462

* flake.{nix,lock}: update Nix derivations

* Set Version: 0.1.170

* flake.{nix,lock}: update Nix derivations

* deps/kevm_release: Set Version 1.0.463

* Sync Poetry files: kevm-pyk version 1.0.463

* flake.{nix,lock}: update Nix derivations

* Updated expected output

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Palina Tolmach <[email protected]>

* Set Version: 0.1.171

* Set Version: 0.1.172

* path correction

* redesigning CSE tests

* slightly more general WETH contract

* minor spacing consistencies

* generalising test harness

* Set Version: 0.1.174

* additional proof options for dependency tests

* AddConst test

* initialisation of accessedStorage

* formatting

* test correction

* adding expected files, WETH9 contract

* correction

* removing accessStorage manipulation, adding full WETH9

* adding nocse kcfgs and updating cse ones

* correction

* Set Version: 0.1.175

* addresses not equal to cheatcode address

* Set Version: 0.1.177

* deps/kevm_release: Set Version 1.0.465

* Sync Poetry files: kevm-pyk version 1.0.465

* flake.{nix,lock}: update Nix derivations

* deps/kevm_release: Set Version 1.0.466

* Sync Poetry files: kevm-pyk version 1.0.466

* deps/k_release: sync release file version 6.3.17

* flake.{nix,lock}: update Nix derivations

* kontrol/{solc_to_k,prove,foundry}: updates from upstream

* src/tests/unit: update expected output

* additional lemmas for discharging infeasible branches

* Set Version: 0.1.178

* caller in accounts

* :integration/test_kontrol_cse.py: init

* updating expected outputs

* Set Version: 0.1.180

* Generate xml report (#377)

* generating a simple xml report

* report with time for each test case

* xml report generated from results of kontrol prove command

* formatted failure text

* Added flag to generate the report only if the --xml-test_report is provided

* execution time in kontrol side

* Set proof execution time

* report with <error> tag for tests that end with exceptions

* report is generated in function foundry_to_xml

* Set Version: 0.1.162

* Formatting

* Added file attribute to testcase

* Set Version: 0.1.163

* Set Version: 0.1.164

* Printing exception trace in the report

* Added CI test for the xml report feature

* Fixed CI test

* Add setup exectuion time to the testsuites

* Fixed testsuites total execution time

* Added one more assertion to CI test

* Added property with kontrol version to xml report

* Set Version: 0.1.165

* Set Version: 0.1.165

* undo changes to profiling test

* Formatting

* Fixed print failure info in xml report

* Set Version: 0.1.179

* Set Version: 0.1.180

* Addressed PR comments

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Palina Tolmach <[email protected]>

* Refactor get_test_id to fetch latest version (#406)

* foundry.py: refactor get_test_id to fetch latest version

* Set Version: 0.1.179

* add docstrings and unit test

* test_foundry_list.py: revert changes

* Set Version: 0.1.180

* foundry-list.expected: revert changes

* test_get_test_id.py: add new unit tests

* foundry.py: refactor get_test_id

* test_get_test_id.py: update fixture and add new test case

* test_get_test_id.py: refactor using monkeypatch

* Set Version: 0.1.181

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: rv-jenkins <[email protected]>

* Remove upper bound from pytest version (#408)

* Remove upper bound from pytest version

* Set Version: 0.1.180

* Set Version: 0.1.181

* Set Version: 0.1.182

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Andrei Văcaru <[email protected]>
Co-authored-by: rv-jenkins <[email protected]>

* Update dependency: deps/kevm_release (#410)

* deps/kevm_release: Set Version 1.0.478

* Set Version: 0.1.180

* Sync Poetry files: kevm-pyk version 1.0.478

* flake.{nix,lock}: update Nix derivations

* Set Version: 0.1.181

* deps/kevm_release: Set Version 1.0.479

* Sync Poetry files: kevm-pyk version 1.0.479

* flake.{nix,lock}: update Nix derivations

* Set Version: 0.1.182

* deps/kevm_release: Set Version 1.0.480

* Sync Poetry files: kevm-pyk version 1.0.480

* flake.{nix,lock}: update Nix derivations

* Set Version: 0.1.183

* deps/kevm_release: Set Version 1.0.481

* Sync Poetry files: kevm-pyk version 1.0.481

* flake.{nix,lock}: update Nix derivations

* Update expected output (w/o `test_foundry_xml_report`)

* deps/kevm_release: Set Version 1.0.482

* Sync Poetry files: kevm-pyk version 1.0.482

* deps/k_release: sync release file version 6.3.25

* flake.{nix,lock}: update Nix derivations

* Reinit proofs in `test_foundry_xml_report`

* Updated expected output w/new exec time format, `terminal` node label

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Palina Tolmach <[email protected]>

* Set Version: 0.1.184

* simplifying lemams and adding them to CI

* Set Version: 0.1.185

* test_kontrol_cse.py: move dependency test from test_foundry_prove

* Set Version: 0.1.188

* test_kontrol_cse.py: refactor test harness

* Set Version: 0.1.192

* Update dependency: deps/kevm_release (#419)

* deps/kevm_release: Set Version 1.0.485

* Set Version: 0.1.188

* Sync Poetry files: kevm-pyk version 1.0.485

* flake.{nix,lock}: update Nix derivations

---------

Co-authored-by: devops <[email protected]>

* skipping tests

* correction

* correction: caller in accounts

* Set Version: 0.1.193

* Set Version: 0.1.194

* removing cbor and hash disabling

* updating expected output

* manual correction of expected output

* adding appropriate expected outputs

* attempting to manually fix expected output

* Set Version: 0.1.195

* adding a CSE CI runner, removing no-cse executions

* removing no-cse.expected files

* updating expected outputs

* Set Version: 0.1.197

* Set Version: 0.1.197

* name correction for CI job

* Update src/tests/integration/test-data/foundry-dependency-all

Co-authored-by: Andrei Văcaru <[email protected]>

* Update src/tests/integration/test-data/foundry-dependency-skip

Co-authored-by: Andrei Văcaru <[email protected]>

* removing unused code

* bringing back execution without CSE for testing purposes

* Set Version: 0.1.200

* adding expected output for no-cse tests

* Set Version: 0.1.202

* Set Version: 0.1.204

* updating expected outputs, correcting non-cse executions

* removing no-cse and updating expected outputs

* Updating the running of proofs

* Set Version: 0.1.205

* adding a skipped test in init tests due to a run-constructor error

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: rv-jenkins <[email protected]>
Co-authored-by: lucasmt <[email protected]>
Co-authored-by: Lucas MT <[email protected]>
Co-authored-by: Palina Tolmach <[email protected]>
Co-authored-by: Everett Hildenbrandt <[email protected]>
Co-authored-by: Andrei <[email protected]>
Co-authored-by: Lisandra <[email protected]>
Co-authored-by: Andrei Văcaru <[email protected]>
Co-authored-by: Tamás Tóth <[email protected]>
@ehildenb ehildenb added the cse label Apr 2, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ehildenb ehildenb ehildenb left review comments

@anvacaru anvacaru anvacaru approved these changes

@palinatolmach palinatolmach Awaiting requested review from palinatolmach

Assignees

@PetarMax PetarMax

Labels
automerge cse enhancement New feature or request
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

External calls in CSE executions
7 participants
@PetarMax @ehildenb @anvacaru @rv-jenkins @lucasmt @lisandrasilva @tothtamas28