Model Verification when Nodes are Trait Objects

[jakehemmerle]

This is what we were starting to get into at the end of 4/17/24 meeting with Antonio and Cesar, but we were getting wiped and out of time. To jog our memory for next time, the new issue is that by refactoring Model to use Vec<Box<dyn NodeOpsCommon>>
as one of its field types, we can't iterate through the nodes on the verifier side and verify the nodes anymore.

So, a few ideas to spur the next discussion:

• I wonder if it makes sense to refactor NodeOpsVerify back into common (gated by a core feature or something), and also refactor its impls gated with a verify feature, which the verifier crate then requires. This allows us to still keep verifier logic out of prover yet still exposes the NodeOpsVerify trait without its impls (via just the core feature), but by recoupling the node verification logic with the nodes themselves (and model verification), verification becomes simpler at the model level.
• Antonio also suggested we might allow the conversion of type Model to another type VerifiableModel, which removes all private data and has a new method that calls verification on the nodes.
• Define NodeOpsCommon as a of supertrait of NodeOpsVerify: By doing this, we need to allow the NodeOpsVerify NodeOpsVerify on the underlying Nodes already. New Nodes will just have to implement NodeOpsVerify
• Merge NodeOpsVerify into NodeOpsCommon, maybe even rename NodeOpsCommon to just NodeOps

[Antonio95]

Thanks a lot for putting this together, @jakehemmerle. You've done an excellent job of capturing the issue and ideas we had! Here are some of my thoughts to bring the rest of the team up to speed and have even more to go off of next time:

• @Cesar199999 and I actually started leaning towards the idea of defining the proof-system-related traits to the common crate. The main reason is that that would allow us to have a very clean definition of a SNARK-like cryptographic primitive in one place, making it easier to relate the code to formal security arguments in papers. To make this a bit more concrete, we started toying with the idea of having a Trait SNARK (read: NodeOps...) in common with the methods setup, prove and verify. Right now, the analogous concept is spread into a Trait NodeOpsVerify with verify in the verifier crate; and a Trait NodeOpsProve with setup and prove in the prover crate (which might not even be public). A small issue I see with this idea is that we'd like to keep the implementation of the proving methods in the prover crate, and of course one cannot have a trait somewhere and implement pieces of that trait in different crates. So a design solution that allows us to keep the full SNARK definition in one crate but implement the proving and verification components in other crates (in some way) would be optimal, IMO.
• As for the VerifiableModel, I am not in love with the design I proposed, but more importantly I suspect it might not be easy to convert a Model into the former - because Model only knows it contains implementors of the NodeOpsCommon subtrait, and not NodeOpsVerify as Model wants. There might be a way around this tho.
• Regarding having NodeOpsCommon as a of supertrait of NodeOpsVerify, that has the issue that we couldn't implement the common methods in the common crate (which we need in order to do things with Model there).
• As for the last solution, I think this would be more organisational than really fix any issues in the sense that, if that did work, then one could just split the traits again and replace any T: NodeOps by T: NodeOpsCommon + NodeOpsVerify. There is, however, an even bigger issue, which is that the whole discussion we are having with verification also applies to proving, and the proving code definitely needs to be in a different crate (because it might even end up not being public).