Make advance proof functionality generic #875

ehildenb · 2024-02-13T17:28:06Z

~~Blocked on: #878~~

In an attempt to make the prover interfaces simpler, we are making it so that advance_proof is a generic method among all *Prover classes. This will allow us to have a generic way to call subproofs and advance them, then call superproofs and advance them, which will allow simplifying some downstream logic a bit.

Makes it so that mlEqualsTrue and mlEqualsFalse can take sort arguments for their outer sort.
Moves all the APRProof specific arguments of APRProof.advance_proof to the constructor instead.
Adds an abstractmethod Proof.step_proof(...) which should take one step of executing a proof to completion.
Adds an abstractmethod Proof.can_progress which lets you know if it's possible to make progress on a given proof.
Implements generic Proof.advance_proof(...) which handles calling step_proof in a loop until either max_iterations is reached, the proof can no longer progress, or if fail_fast trigger hits. It also handles writing proof data each iteration.
Adjusts all the tests to the new interface.

ehildenb · 2024-02-13T21:26:45Z

KEVM is updated here to handle this new interface: runtimeverification/evm-semantics#2294

I made a PR here #875 which caused CI to jump from 8 minutes to an infinite loop. We shouldn't let CI machines be taken up because of mistakes in PRs. This also adds the pytest-timeout module so we can do `make cov-integration COV_ARGS='--timeout 300'` to timeout individual tests. --------- Co-authored-by: devops <[email protected]> Co-authored-by: rv-jenkins <[email protected]>

While working on #875, I found many places in `ImpliesProof` class hierarchy that we can make things simpler. In general: - `mlEqualsTrue` and `mlEqualsFalse` are given sorts they can use for the outer sort of the equality. - The various renaming of `antecedent` and `consequent` in subclasses are removed. - The `ImpliesProof` gets its own `dict` and `from_dict` methods, and the subclasses and reuse it. - `advance_proof` no longer needs to be overloaded in the subclasses. - Various really simple setter methods are removed in favor of direct setting of paramaters in the proofs. - The now-useless classes `EqualityProver` and `RefutationProver` are removed. Essentially, after this, `EqualityProof` and `RefutationProof` are just "smart constructors" for `ImpliesProof`, with different names for the antecedent/consequent and specific ways of constructing the antecedent/consequent. The key difference here is that `EqualityProver` and `RefutationProver` were tracking their own proof state before (by storing and manipulating `_antecedent_kast` and `_consequent_kast` themselves directly), and now they rely only on the `*Proof` objects to store state. --------- Co-authored-by: devops <[email protected]>

…erations

…Prover.step_proof

…n_progress to control iterations

I made a PR here runtimeverification/pyk#875 which caused CI to jump from 8 minutes to an infinite loop. We shouldn't let CI machines be taken up because of mistakes in PRs. This also adds the pytest-timeout module so we can do `make cov-integration COV_ARGS='--timeout 300'` to timeout individual tests. --------- Co-authored-by: devops <[email protected]> Co-authored-by: rv-jenkins <[email protected]>

While working on runtimeverification/pyk#875, I found many places in `ImpliesProof` class hierarchy that we can make things simpler. In general: - `mlEqualsTrue` and `mlEqualsFalse` are given sorts they can use for the outer sort of the equality. - The various renaming of `antecedent` and `consequent` in subclasses are removed. - The `ImpliesProof` gets its own `dict` and `from_dict` methods, and the subclasses and reuse it. - `advance_proof` no longer needs to be overloaded in the subclasses. - Various really simple setter methods are removed in favor of direct setting of paramaters in the proofs. - The now-useless classes `EqualityProver` and `RefutationProver` are removed. Essentially, after this, `EqualityProof` and `RefutationProof` are just "smart constructors" for `ImpliesProof`, with different names for the antecedent/consequent and specific ways of constructing the antecedent/consequent. The key difference here is that `EqualityProver` and `RefutationProver` were tracking their own proof state before (by storing and manipulating `_antecedent_kast` and `_consequent_kast` themselves directly), and now they rely only on the `*Proof` objects to store state. --------- Co-authored-by: devops <[email protected]>

I made a PR here runtimeverification/pyk#875 which caused CI to jump from 8 minutes to an infinite loop. We shouldn't let CI machines be taken up because of mistakes in PRs. This also adds the pytest-timeout module so we can do `make cov-integration COV_ARGS='--timeout 300'` to timeout individual tests. --------- Co-authored-by: devops <[email protected]> Co-authored-by: rv-jenkins <[email protected]>

While working on runtimeverification/pyk#875, I found many places in `ImpliesProof` class hierarchy that we can make things simpler. In general: - `mlEqualsTrue` and `mlEqualsFalse` are given sorts they can use for the outer sort of the equality. - The various renaming of `antecedent` and `consequent` in subclasses are removed. - The `ImpliesProof` gets its own `dict` and `from_dict` methods, and the subclasses and reuse it. - `advance_proof` no longer needs to be overloaded in the subclasses. - Various really simple setter methods are removed in favor of direct setting of paramaters in the proofs. - The now-useless classes `EqualityProver` and `RefutationProver` are removed. Essentially, after this, `EqualityProof` and `RefutationProof` are just "smart constructors" for `ImpliesProof`, with different names for the antecedent/consequent and specific ways of constructing the antecedent/consequent. The key difference here is that `EqualityProver` and `RefutationProver` were tracking their own proof state before (by storing and manipulating `_antecedent_kast` and `_consequent_kast` themselves directly), and now they rely only on the `*Proof` objects to store state. --------- Co-authored-by: devops <[email protected]>

~Blocked on: runtimeverification/pyk#878 In an attempt to make the prover interfaces simpler, we are making it so that `advance_proof` is a generic method among all `*Prover` classes. This will allow us to have a generic way to call subproofs and advance them, then call superproofs and advance them, which will allow simplifying some downstream logic a bit. - Makes it so that `mlEqualsTrue` and `mlEqualsFalse` can take sort arguments for their outer sort. - Moves all the `APRProof` specific arguments of `APRProof.advance_proof` to the constructor instead. - Adds an `abstractmethod Proof.step_proof(...)` which should take one step of executing a proof to completion. - Adds an `abstractmethod Proof.can_progress` which lets you know if it's possible to make progress on a given proof. - Implements generic `Proof.advance_proof(...)` which handles calling `step_proof` in a loop until either `max_iterations` is reached, the proof can no longer progress, or if `fail_fast` trigger hits. It also handles writing proof data each iteration. - Adjusts all the tests to the new interface. --------- Co-authored-by: devops <[email protected]>