Factor out vat arithmetic in proof-reuse for MCD #2467
Merged
Conversation
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
…needed dependencies
…st-pyk-prove test-suite
…of_rules to run test-prove-dss
rv-jenkins
pushed a commit
to runtimeverification/k
that referenced
this pull request
Jun 12, 2024
…4427) Currently, when we are generating lemmas from subproofs to be included in superproofs, we include each basic block of execution of the subproof directly as a rule for execution during the superproof. This means that we mirror the branching structure of the subproof directly, and aren't able to reduce the branching factor. However, when writing proofs that involve loop invariants or branching as `KClaim`, the user often provides the _exact_ final state that matters, even if it's reached in multiple different ways on different branches. For example, in the MCD proof suite, the `Vat.frob` proof: https://github.com/runtimeverification/evm-semantics/blob/20a292412797498f9eb70486aef19cd2f99cd9f2/tests/specs/mcd/vat-frob-diff-zero-dart-pass-rough-spec.k#L7 End up reusing several of the `Vat.` arithmetic proofs, like `Vat.muluu` several times: https://github.com/runtimeverification/evm-semantics/blob/20a292412797498f9eb70486aef19cd2f99cd9f2/tests/specs/mcd/vat-frob-diff-zero-dart-pass-rough-spec.k#L288 If this subproof is included directly as its basic blocks as learned lemmas, then we arrive to a situation where we aren't actually reducing the branching factor in the superproof, even though the `Vat.muluu` specification already describes exactly the behavior that happens on all 3 branches of that proofs. This PR introduces an `direct_subproof_rules: bool = True` field to the `APRProver` class, so the user can specify whether they want this behavior or not. - A few logging messages are added to `APRProver.advance_proof` to help with debugging proofs that fail early. - The lemma generation process is handled more directly in `APRProof.as_rules`, instead of in `APRProve.init_proof`, which now can just call `APRProof.as_rules` directly without any extra processing of the results or deciding how to turn it into lemmas. - The field `direct_subproof_rules` is added to the `APRProver` class. - When building lemmas in `APRProver.init_proof`, we use the field `direct_subproof_rules` to determine how to build lemmas from subproofs. - The `APRProof.as_rules` changes its behavior on whether `direct_rule` is set or not. If `direct_subproof_rules` is set and the proof is passing, instead of building the lemmas as the basic blocks in the KCFG, we build it directly from the initial node to the target node of the KCFG. This improves the performance of the KEVM MCD Vat Proof suite dramatically in [this PR](runtimeverification/evm-semantics#2467): ``` spec | original time | new time VAT-ADDUI-FAIL-ROUGH-SPEC.Vat.addui.fail.rough | 38.32540s | 38.8101s VAT-ARITHMETIC-SPEC.Vat.adduu.pass | 21.32606s | 20.8181s VAT-ARITHMETIC-SPEC.Vat.mului.pass | 72.18441s | 71.2940s VAT-ARITHMETIC-SPEC.Vat.muluu.pass | 84.01074s | 68.8481s VAT-ARITHMETIC-SPEC.Vat.subui.pass | 104.4093s | 105.154s VAT-ARITHMETIC-SPEC.Vat.subuu.pass | 20.32957s | 21.4818s VAT-DAI-PASS-SPEC.Vat.dai.pass | 10.81132s | 10.5747s VAT-DENY-DIFF-FAIL-ROUGH-SPEC.Vat.deny-diff.fail.rough | 58.88762s | 55.3194s VAT-FLUX-DIFF-PASS-ROUGH-SPEC.Vat.flux-diff.pass.rough | 45.90303s | 45.7166s VAT-FLUX-DIFF-PASS-SPEC.Vat.flux-diff.pass | 46.53391s | 44.7944s VAT-FOLD-PASS-ROUGH-SPEC.Vat.fold.pass.rough | 380.6935s | 107.786s VAT-FORK-DIFF-PASS-ROUGH-SPEC.Vat.fork-diff.pass.rough | 10961.03s | 466.333s VAT-FROB-DIFF-ZERO-DART-PASS-ROUGH-SPEC.Vat.frob-diff-zero-dart.pass.rough | 4382.788s | 992.793s VAT-HEAL-PASS-SPEC.Vat.heal.pass | 34.03113s | 28.5053s VAT-MOVE-DIFF-ROUGH-SPEC.Vat.move-diff.pass.rough | 38.68574s | 40.4618s VAT-SIN-PASS-SPEC.Vat.sin.pass | 10.80752s | 10.5180s VAT-SUBUI-FAIL-ROUGH-SPEC.Vat.subui.fail.rough | 35.38427s | 36.0153s ```
anvacaru
approved these changes
Jun 13, 2024
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Blocked on: #2451Blocked on: runtimeverification/k#4427Blocked on: #2481To test better our subproof mechanisms and proof re-use, this factors out the MCD proof-suite to use the new
depends(...)mechanism which the RPC server needs for listing dependencies between proofs.--direct-subproof-rulesis added tokevm prove ...which tells it to interpret subproofs directly for lemma generation, rather than including every basic block in their KCFG. Related: Allow specifying that an APRProof generated lemmas should be direct k#4427tests/specs/mcd/vat-arithmetic-spec.kis added which has the positive cases of all the Vat contract arithmetic functions verified.vat-arithmetic-spec.kinstead.tests/specs/mcd/vat-spec.kincludes all the vat specifications as the new main super-spec for those proofs.kprove,kore-rpc,kore-rpc-booster, andbooster-dev).vat-spec.kproof-suite in parallel directly as a single proof tree using thekore-rpc-booster, and runs the proofs in parallel with up to 8 workers.With the factored out proof reuse working on the RPC server, we now have much better runtimes of the longest running Vat proofs:
TODO: Update the required status checks to include the new
test-prove-dss.