Add parameter to advance_proof to split into subproofs after enough branches have been created
#638
Conversation
…ication/pyk into noah/subproof-split
src/pyk/proof/reachability.py
Outdated
| _LOGGER.info(f'Delegating node {node.id} to a new proof.') | ||
| subproof = self.construct_node_subproof(node) | ||
| self.proof.add_subproof(subproof) | ||
| self.proof.kcfg.add_stuck(node.id) |
There was a problem hiding this comment.
Hmmmm, adding stuck to this node will make it marked as failing, won't it? Maybe instead ew should treat it the same way we treat refutations, by tracking a list of subproof_nodes or something, and linknig that node to the subproof. That way we are correctly reporting pass/fail state of the overall proof.
|
The main purpose of splitting to subproofs was to make parallelism easier. So we need to see if that will actually accomplish that goal. If not, do we need to do this? I guess we also get benefit of focusing on the subproblem, and being able to pass that around with less data? |
|
@ehildenb What do we need to see with regard to whether or not it will make parallelism easier? As you say, adding |
|
Ohhhh, nice. That looks good. Please discuss with Tamas in yoru meeting, see if it's an appropriate solution. Thanks for making an example with KEVM! |
…everification/pyk into noah/extract-branches-fix
…ication/pyk into noah/subproof-split
…ication/pyk into noah/subproof-split
…ication/pyk into noah/subproof-split
| ) | ||
| for pending_node in self.proof.pending: | ||
| self.delegate_to_subproof(pending_node) | ||
| break |
There was a problem hiding this comment.
Can delegate_to_subproof result in new pending nodes for self.proof?
There was a problem hiding this comment.
It shouldn't create any new nodes in self.proof, no.
…ication/pyk into noah/subproof-split
|
Blocked on runtimeverification/evm-semantics#2094 |
In #524 @ehildenb suggested that we would want to have an option to split proofs off as subproofs if too much branching (too many pending nodes) happens in one proof. This would also be used to facilitate parallelization of a single proof, by allowing it to split itself into subproofs which could be executed independently.