-
Notifications
You must be signed in to change notification settings - Fork 1
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
Notes from review of transparent instantiation #21
Comments
The engineering time suggested using this as a workaround to mock up the missing blob storage. We didn't want to store the
The engineering team said that these are not required. We went over the missing definitions in a meeting with Ray. We had the same questions and didn't understand why these are not required.
The idea was to have clearly separated spheres of responsibility. If an instantiator makes changes to their implementation (e.g., how commitments are computed - the transparent RM, for example, appends/prepends the word "committo" to the resource object) the Juvix side shouldn't need to adapt the code. RM instantiators should maintain the interface to their RM (which contains all the functions that the general Juvix interface) must use. |
Do I understand that this opaque type will be removed now then (since we're adding simple blob storage)?
Yes, I think this has been clarified (and we should define them properly in the Juvix code).
I see. For commitments and nullifiers, this makes sense to me, it's nice that the transparent RM could change implementation details without developers needing to change their programs. I think in that case implementing these functions as builtins in the Juvix Nock interpreter is sufficient. For transaction composition, I still don't think this makes sense, as the transaction data type is defined in Juvix anyways - it would never make sense for the transparent implementation to redefine what composition means. Do you think the boundary there makes sense? |
Yes. We don't need it.
Yes, for transaction composition, this makes sense. A boundary that Paul and I were thinking about is that all computations being required for verification should come from the node. If the Juvix verification mechanism would not have the exact same semantics but deviate from the node, this could potentially be problematic, i.e., if in some scenarios the same input arguments can result in a different verification outcomes. |
In practice, the node will not actually run the Juvix verification functions, but we want to be very clear on exactly what the verification semantics are, and we can cross-test - in effect, once the Juvix code is merged into the specs, it should be a spec-as-code that we can use e.g. to generate testcases and have automatic "specs compliance tests". |
That sounds good to me. Ping @paulcadman for visibility. |
Yes I keep forgetting that the Juvix RM code has multiple purposes. These include:
|
I implemented |
Notes from review of transparent instantiation by @cwgoes 2024.10.31 (not yet fully organized into tasks).
Note that I have not duplicated my comments from #17.
TrivialProof
proof scheme) - is not "not required" - it must check the computation by performing the computation. I believe @vveiln is clarifying this in the specs. I'm confused as to how this resource machine is expected to verify properties if these proofs aren't really checked - is this the result of trying to adapt to something done by the current transparent RM code on the node side?Delta
here. If it's easier, defining all the builtins in Juvix (or Haskell) is alright too, but it seems to me like we might (a) have more builtins than necessary (simple string operations do not need to be builtins), and (b) not have builtins that we should (e.g. hash functions, I heard that we were trying to implement one directly in Juvix).I want to do a second review pass, but maybe this is enough to start with for now.
The text was updated successfully, but these errors were encountered: