Implement structural checkers for proofs

runtimeverification / evm-semantics

K Semantics of the Ethereum Virtual Machine (EVM)

BSD 3-Clause "New" or "Revised" License

506 stars 140 forks source link

Implement structural checkers for proofs #1994

Open tothtamas28 opened 1 year ago

tothtamas28 commented 1 year ago

This would enable us to verify foundry_prove test results structurally, as opposed to comparing foundry_show output to an expected string, which is very brittle.

ehildenb commented 1 year ago

What we really want to test is something like:

Same graph structure overall.
Same depth of each basic block.
Same branching conditions.
Same end conditions.
Roughly same configuration each state.

Comparing the string output roughly approximates that, but doing it structurally would be better. Maybe we store the actual KCFGs and have an intentional way of diffing them (or the APRProof)?

tothtamas28 commented 1 year ago

Renamed the PR and edited the description to better reflect this goal.