Overhaul ImpliesProof class hierarchy #878

ehildenb · 2024-02-14T00:00:05Z

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.

ehildenb · 2024-02-14T16:59:41Z

Changes to KEVM to make it build successfully with this change are in this branch: runtimeverification/evm-semantics#2294

…t/consequent

…r and EqualityPRover

…ationProver

…us to ImpliesProof.status

~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. --------- 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]>

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]>

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]>

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]>

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]>

ehildenb self-assigned this Feb 14, 2024

ehildenb mentioned this pull request Feb 14, 2024

Make advance proof functionality generic #875

Merged

ehildenb force-pushed the equality-proof-overhaul branch from 3f7e975 to 74803bb Compare February 14, 2024 16:35

ehildenb mentioned this pull request Feb 14, 2024

[NO-MERGE] Changes needed for successful build runtimeverification/evm-semantics#2294

Closed

ehildenb added 10 commits February 14, 2024 18:53

proof/equality: ImpliesProver does not carry around its own anteceden…

10dd69e

…t/consequent

prelude/ml: allow mlEqualsTrue/mlEqualsFalse to specific outer sort

003f514

proof/equality: get rid of setter methods for proof manipulation

4fdfbff

proof/equality: EqualityProof makes use of ImpliesProof existing fields

3f85dd0

proof/equality: RefutationProof reuses superclass variables

ae1f933

proof/{equality,__init__}: remove now useless classes RefutationProve…

152e266

…r and EqualityPRover

proof/{equality,reachability}: remove unused argument sort from Refut…

7f60272

…ationProver

proof/equality: promote EqualityProof.status and RefutationProof.stat…

bed0d8a

…us to ImpliesProof.status

proof/equality: remove ImpliesProof.set_csubst

d21eafa

proof/equality: turn fields of EqualityProof into propertiees

c01aeff

ehildenb force-pushed the equality-proof-overhaul branch from 7108637 to c01aeff Compare February 14, 2024 20:00

ehildenb and others added 2 commits February 14, 2024 20:00

Merge c01aeff into 6d723fd

2be181d

Set Version: 0.1.626

aa0da35

ehildenb marked this pull request as ready for review February 14, 2024 20:18

ehildenb requested a review from nwatson22 February 14, 2024 20:18

nwatson22 approved these changes Feb 14, 2024

View reviewed changes

ehildenb added the automerge label Feb 14, 2024

rv-jenkins merged commit 9453af7 into master Feb 14, 2024

rv-jenkins deleted the equality-proof-overhaul branch February 14, 2024 21:43

ehildenb mentioned this pull request Feb 14, 2024

Update dependency: deps/pyk_release runtimeverification/evm-semantics#2300

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Overhaul ImpliesProof class hierarchy #878

Overhaul ImpliesProof class hierarchy #878

Uh oh!

ehildenb commented Feb 14, 2024 •

edited

Loading

Uh oh!

ehildenb commented Feb 14, 2024

Uh oh!

Uh oh!

Overhaul ImpliesProof class hierarchy #878

Overhaul ImpliesProof class hierarchy #878

Uh oh!

Conversation

ehildenb commented Feb 14, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ehildenb commented Feb 14, 2024

Uh oh!

Uh oh!

ehildenb commented Feb 14, 2024 •

edited

Loading