Proof container proof type

[nwatson22]

Adds MultiProof proof type which is just a container to hold other proofs as subproofs. This is for kontrol, so instead of having proofs that are setUp proofs, constructor proofs, and main test function proofs grafted together into a single CFG, we can have these as separate CFGs under a single MultiProof.

See: runtimeverification/kontrol#481 (comment)

Also fixes Proof.subproofs property so that it does what it says in the docstring (updates the subproofs from disk if they changed). This uncovered a bug in one of the ImpliesProof tests occurring when converting an ImpliesProof to a RefutationProof where we were adding an true #Equals ... to #Top which got triggered when reloading the RefutationProof from disk.

[ehildenb]

Why does this need to be its own class? Doesn't Proof already hold multiple subproofs?

[nwatson22]

Why does this need to be its own class? Doesn't Proof already hold multiple subproofs?

@ehildenb The only real reason is that Proof is abstract. But we could alternatively just make Proof instantiable and use that for the same purpose.

[tothtamas28]

Why does this need to be its own class? Doesn't Proof already hold multiple subproofs?

@ehildenb The only real reason is that Proof is abstract. But we could alternatively just make Proof instantiable and use that for the same purpose.

But e.g. APRProof is concrete and has subproofs. Would that cover your use case?

In general, I see how having a MultiProof could be a good way to represent composite proof obligations. The problem is, a prover of a given proof type depends on the type of the subproofs, since it needs to incorporate subproof results into the proving process somehow.

[PetarMax]

I am also not understanding the gap between the current and the desired functionality. Any proof can have subproofs, and they needn't be the same type of proof as the superproof.

We could structure the analysis process in Kontrol differently, so that setUp functions are registered as proper subproofs, etc.

[nwatson22]

We could structure the analysis process in Kontrol differently, so that setUp functions are registered as proper subproofs, etc.

@PetarMax We could and this would make some sense, but the idea is that, to be able to support proofs with branching setUp, we make one APRProof for each leaf of the setUp KCFG. These would all be co-equal so it wouldn't make sense to put them in a subproof relation to each other, and also it doesn't really make sense to make them all subproofs of the setUp proof.

[nwatson22]

But e.g. APRProof is concrete and has subproofs. Would that cover your use case?

@tothtamas28 Technically yes, but I'm trying to do this in a way that is clean and would be intuitive to the user. With the use case here there's no obvious single proof that is logically the superproof of everything else. We could make a dummy APRProof that fulfills the same "container" purpose, but that would have superfluous properties.

In general, I see how having a MultiProof could be a good way to represent composite proof obligations. The problem is, a prover of a given proof type depends on the type of the subproofs, since it needs to incorporate subproof results into the proving process somehow.

Subproofs can already be of mixed types/different types from the superproof. APRProver uses the subproofs of its APRProof, but it limits itself to considering those of specific types, APRProof and RefutationProof. There is no proving logic for MultiProof (it is considered to be own_status=passing with no available steps, and there is no associated Prover type). Subproofs of existing proof types are discharged separately by provers of their own appropriate type, and it is the same here with subproofs of MultiProof.

[tothtamas28]

(Continuing the discussion here to form a thread.)

What feature of a Proof does this class rely on, what makes it different from, say, a list[Proof]?

[nwatson22]

It would be the logic in Proof.status which tracks the status of the subproofs to tell when the whole proof has been discharged, and the ability to save/load from disk.

[PetarMax]

(forming a thread)

I would like to make the use case very precise. Imagine that we did have a branching setUp, with all of its final states, together with the proofs of the associated test for each of the branches. How are these connected in the MultiProof? How do I know which proof corresponds to which branch? Could you give an example - imagine setUp branches into 3 possibilities.

Also, from the test below, I see that subproof_ids are used, but I don't see a proof that's their superproof.

[nwatson22]

I was thinking the constructor proof, setUp proof(s), and the main proof(s) could just go directly under one MultiProof.

To know which proof corresponds to each branch, we would probably set the proof ID of the test function subproofs to something which included the node ID of the setUp KCFG it copies its starting configuration from. So if the function is called my_test, and the setUp function branches into 3 and ends on nodes 10, 11, and 12, the subproof graph could look something like:

[MyContract.my_test (MultiProof)]-->(
    [MyContract.setUp (APRProof)], 
    [MyContract.my_test_setup_config_10 (APRProof)], 
    [MyContract.my_test_setup_config_11 (APRProof)], 
    [MyContract.my_test_setup_config_12 (APRProof)], 
)

And of course you can also inspect the initial configurations of the subproofs.

[PetarMax]

Thoughts, @tothtamas28, @ehildenb?

[tothtamas28]

I guess the subproof abstraction cannot be used here because in kontrol these proof obligations are manually constructed from one another. i.e.

init -> constructor done
constructor done -> setup done
setup done -> target
------------------------------
init -> target

is done by hand (i.e. not by the prover backend).

I wonder, would it be possible to use subproofs if we changed the semantics? Because in a semantics where constructor and setup steps are handled internally, this sequential compositon can be handled by the backend.

[tothtamas28]

Example to better highlight the difference between subproofs and MultiProof as I understand it. Suppose we want to prove a -> c.

Subproof approach:

claim: a -> c
sub-claim: a -> b

If the proof passes, we know a -> c. The sub-claim might make proving more efficient, or might even be necessary for a -> c to pass.

MultiProof approach:

sub-claim: b -> c
sub-claim: a -> b

If the MultiProof passes, we know a -> c, but just because we constructed it so. The composition or the original calim a -> c is never machine-checked.