-
Notifications
You must be signed in to change notification settings - Fork 145
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Check if pre-branch node is subsumed in AGProver, add CTerm.cell (#340)
Currently, if we have a proof that reaches a branch-point, and the pre-branch state is subsumed into the target state, it will still compute the branches, and then check each post-branch state individually for subsumption into the target state. The branches are still subsumed into the target, but it makes the KCFG more complicated because it has the uneeded branch there. This PR: - Adds a test where subsumption happens at a branch point, and fails because we set it to only do one iteration of extending the prover (passes after these changes). - Factors out the final subsumption check into its own routine, and calls it on new frontier nodes as well as on new pre-branch nodes. - Adds a helper getter `CTerm.cell(...)` as a shortcut to `get_cell(CTerm.config, ...)` - Removes the unused parameter `simplify_init` to `AGProver.advance_proof(...)`. It has been tested on [this proof](https://github.com/runtimeverification/evm-semantics/blob/master/tests/specs/mcd/vat-addui-pass-spec.k), which is subsumed right at the branch point, and does indeed produce a smaller KCFG. This proof was introduced by @dkcumming in order to work on proof-reuse in the larger still-failing proofs in KEVM test-suite. With this change, we reduce the branching factor of the proof from 6 to 3. The overall runtime goes from ~4min to ~3min40s (not much change), and the number of queries to the RPC server goes from 26 to 25 (not much change). Overall this will increase the number of implication checks we make, but still not nearly as many as the original prover made. The test added fails before the change because with `--max-iterations=1` set, it never makes it to checking subsumption into the target state once it hits the branch point on the `if(...) ...` statement. But with this change, it checks subsumption into the target state as soon as it's made the first basic block, and the proof is discharged. --------- Co-authored-by: devops <devops@runtimeverification.com>
- Loading branch information
Showing
9 changed files
with
58 additions
and
30 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1 +1 @@ | ||
0.1.225 | ||
0.1.226 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters