-
Notifications
You must be signed in to change notification settings - Fork 160
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merging two MAST forests together #1529
Comments
Here is what I think we want to do here: Given two MastForest structs, we should merge them together (we can also generalize this beyond just 2 structs). The resulting I suspect that handling of duplicates will probably be one of the more complicated parts (because we need to compare based not just on MAST root but also on "eq hash"). We could try to use a similar strategy as what we use in MastForestBulder - but maybe there is a simpler way as well. |
Thanks! I wrote down my understanding and approach and some questions. To merge two Nodes To combine the
To give an example for both points: Suppose we have some forest A with these nodes:
and merge some forest B into it:
then we should get:
Roots
Implementation Using the Open Questions
|
Yes, this pretty much exactly correct. A few comments:
Yes, but I think we also need to merge the decorators.
Agreed! I don't think we can use
If The main point of external nodes is to say "the definition of this MAST node is not available within this MAST forest". And so, since the union of
This is one of the tricky aspect of the MAST forest and I'll tag @plafer here as well in case my explanation is missing something. But basically, yes, it is possible to have two or more nodes with the same MAST root in the MAST forest (but I don't think that's possible for roots). Semantically, such nodes should be identical - i.e., executing either of them should have exactly the same effect as decorators should not affect how a program is executed (decorators should mostly be used for debug purposes). This is not entirely true now - but should be true once #1457 is completed. |
Indeed, that is a current quirk of the design, and has been the focus of many discussions. From program verification's standpoint, the MAST root fully identifies a program. Decorators were introduced to direct the prover that do things that are really an implementation detail from proof verification standpoint (such as outputting a debug message, or writing something to the advice stack). The problem that this introduces then, especially when using external libraries, is that programs identify procedures to execute by their MAST root, but that turns out to be insufficient information for the prover, as 2 procedures with the same MAST root can differ e.g. in the debug statements they output. Our almost-perfect solution (with #1457) is to turn the decorators that do non-debug things to instructions (i.e. they will now modify the MAST root). Hence, after #1457, theoretically the only quirk in program execution that occurs is that the prover ends up executing the correct procedures but with the wrong debug instructions (in the case where 2 procedures are identical except for e.g. their print statements). As discussed at length, we currently evaluate the probability of this case to happen to be quite low - and we'll be forced to revisit this if it turns out to occur more than we expected. |
Closed by #1534 |
@PhilippGackstatter to create the issue. @bobbinth can help to define the issue
The text was updated successfully, but these errors were encountered: