Notes from review of transparent instantiation

[cwgoes]

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 https://github.com/anoma/juvix-arm-specs/issues/17.

• Why do we need this "AnomaOpaque" type (here)? When are we dealing with data which is untyped (in Juvix)?
• The verification for trivial proofs (here, here - maybe more, and these should actually all be one function, on a 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?
• As I understand commitment and nullifier computation (encode the value and add a prefix), I think we should be able to implement this directly in Juvix, I don't quite see why we need a builtin (though it's fine to have one). At the very least, we need a real implementation in Juvix anyways for the model to be complete - we can replace that implementation with a built-in when compiling if it's better for speed reasons.
• Ditto for a bunch of these functions which appear to be only externally defined as builtins, e.g. 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).
• The verifyAction and verifyTransaction functions are definitely required. Similar comment to above.
• Why does transaction composition need to be a built-in?

I want to do a second review pass, but maybe this is enough to start with for now.

[heueristik]

Why do we need this "AnomaOpaque" type (here)? When are we dealing with data which is untyped (in Juvix)?

The engineering time suggested using this as a workaround to mock up the missing blob storage. We didn't want to store the Logic function in the resource like they are doing it for the testnet (because this would have been recursive (since the logic inputs are resources)). Besides for this workaround, there is no need for opaque types.

The verification for trivial proofs (here, here - maybe more, and these should actually all be one function, on a 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?

The verifyAction and verifyTransaction functions are definitely required. Similar comment to above.

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. Today, we discussed this in our RM team standup.

As I understand commitment and nullifier computation (encode the value and add a prefix), I think we should be able to implement this directly in Juvix, I don't quite see why we need a builtin (though it's fine to have one). At the very least, we need a real implementation in Juvix anyways for the model to be complete - we can replace that implementation with a built-in when compiling if it's better for speed reasons.

Ditto for a bunch of these functions which appear to be only externally defined as builtins, e.g. 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).

Why does transaction composition need to be a built-in?

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.

[cwgoes]

The engineering time suggested using this as a workaround to mock up the missing blob storage. We didn't want to store the Logic function in the resource like they are doing it for the testnet (because this would have been recursive (since the logic inputs are resources)). Besides for this workaround, there is no need for opaque types.

Do I understand that this opaque type will be removed now then (since we're adding simple blob storage)?

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. Today, we discussed this in our RM team standup.

Yes, I think this has been clarified (and we should define them properly in the Juvix code).

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.

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?

[heueristik]

Do I understand that this opaque type will be removed now then (since we're adding simple blob storage)?

Yes. We don't need it.

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, 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. Do you think this is a concern?

[cwgoes]

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. Do you think this is a concern?

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".

[heueristik]

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.

[paulcadman]

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:

1. code for a library to interact with the RM instantiation
2. code to include in the RM specification

[heueristik]

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.

I implemented composeTransactions in https://github.com/anoma/juvix-arm-specs/pull/22