RM interoperability questions and concerns

Resource Machine Stuff
1

Please list here all questions and concerns regarding interoperability between transparent and shielded resource machines, where the desired goal is to be able to use any instruction sets and proving systems (for resource logics) and any combination of transparent and shielded resources in the same transaction, such that there no longer need to even be a concept of a “transparent RM” or “shielded RM” at that level.

2

This is a work in progress reply, but I’m posting it here because it can already be useful.

I think it makes sense to talk about at least three degrees of interoperability:

  1. having both transparent and shielded resources of the same RM in the same transaction
  2. having resources of different RMs in different transactions
  3. having resources of different RMs in the same transaction

The first one seems to be conceptually quite simple since shielded resources can easily be turned into transparent, so the only concern there would be to make sure that the spec:

  1. doesn’t prevent some shielded operations
  2. doesn’t underspecify some structures in a way that makes it easy to exploit the system (following the spec + the shielded guidelines should be sufficient to have the desired guarantees)
  3. something else i forgot

TODO: analyse the state of the spec in that regard right now

The second option should generally work fine if whoever creates/consumes/verifies the transaction:

  1. can figure out what RM should be used - from what I understand, this part is enabled by the use of multiformats
  2. has access to that RM - this is the actor’s responsibility, I suppose
  3. has general interface that is parametrised by the RM in use - the spec aims to describe such an interface

So this part seems to be taken care of as well.

Now, the third one is where a lot of things break:

  1. Transaction delta proving system is defined by an RM instantiation. If there are multiple RMs in use, what delta proving system and delta hash should be used?
  2. Resource kind derivation scheme is also determined by the RM instantiation, so the same pair (label, logic) might be translated into different kind values in different RMs because of different derivation schemes or the kind itself or the hash functions used to derive labelRef or logicRef. Having different resource kinds also breaks the delta computation even if the delta hash / proving system are agreed on
  3. if we consider a “raw” resource a collection of resource components before the application of various hashes (so label instead of labelRef, etc), then different RMs can have the same resource (same raw components, but different hashes if different hash functions are used) exist at the same time. I’m not sure it is a big problem, but I think it makes sense to make it explicit and think if it could break anything
  4. thinking

Another thing we discussed before and I think is related to interoperability is how to switch between proof types (trivial, delegated, zk) without requiring different logic signatures. These proof types imply different distribution of instance/witness inputs the way we defined them, and therefore the same logic might not work with all proof types or not meet the expected guarantees. The simple solution would be to ask the app devs to write inputs and constraints in the way they would write them for zk proving systems (if they want to support shielded execution) and have an intermediate processor that moves the inputs around in case a trivial/delegated proof is required

1 Like
3

Thanks for the response - a few clarification questions from my end:

What about allowing a transaction to have multiple delta proofs, which could potentially use different proving systems (similar to how we’d allow different RL proofs to use different proving systems)? As long as we can add delta values together and verify that the overall transaction delta is zero, I’d imagine that this could work?

In general, it should be safe to treat resources that might be “morally fungible” (expressions of the same function in different resource logic VMs, with different consequent logic references and kinds, for example, or even the same logic with different hashes using different hash functions) as not fungible, as long as we don’t do the reverse. I think as a start we could simply allow explicit conversion (if an application is compiled to RL 1 for backend 1 and RL 2 for backend 2, the compiler knows that RL 1 and RL 2 are equivalent, and it could add in logic to RL 1 and RL 2 to allow conversion to/from resources with the other logic). Do you think this approach could work?

Yes, I think we should really attempt to standardize this, even if the changes a developer would need to make are minimal, the difference between “no changes for a different backend” and “minimal changes” matters a lot in practice.

1 Like
4

I have a few concrete questions:

  • Do we want to support the idea that transparent and shielded resources should be identical? For instance, are transparent ‘ETH’ resources treated the same as shielded ‘ETH’ resources? If so, we could use any underlying RMs interchangeably. This would be an ideal model, although it may be challenging to implement in practice. At the very least, we need to unify all basic structs (e.g., fields) and primitives (e.g., hash functions, commitment, nullifier derivation, kind computation) used in all RMs. Alternatively, they can be considered separate resources but cross-referenced.
  • Do we want to support multiple RMs in a single action? The action represents the minimal execution context, as any circuits (compliance and logic) in a shielded environment can only access data within the scope of the action. There may be issues if transparent logic is allowed to access shielded resources. Essentially, it’s a question of whether it’s reasonable to allow a mixture of transparent and shielded logics in the same execution context (action). If only one type of RM is permitted per action and multiple actions (RMs) can be combined in one transaction, the interoperability might be clearer and easier, although not perfect. The main concern then becomes compatibility of delta proof between RMs.
2 Likes
5

In principle, yes, but I agree that this may be challenging to implement in practice, and doing it without performance tradeoffs may require some pretty complex logic (e.g. in terms of which hash functions to use when). Separate resources which are cross-referenced and can be converted is probably a pretty viable solution for the time being.

If it simplifies the complexity of interoperability, I think we can probably say that each action has only one set of RM primitives for now. This may entail using intent resources to carry constraints across actions more than we might otherwise need to, which is a little bit suboptimal, but it’s not a huge deal. What do you think @vveiln ?

1 Like
6

Are they the same proofs or what is the difference between them, besides the proving system?

I think the difference here is that RL proofs are independent, and delta proofs are meant to be composable

Yeah, explicit conversion would work as long as some party keeps track of the allowed conversions explicitly

1 Like
7

Yeah, having that would compromise the privacy of the shielded resources, so we should prohibit that.

I think it is a good idea, otherwise it would also be challenging to validate resource objects of different RMs: if cm = h(r), how does the logic know which h to use for which r? It might be easier to do in the transparent case, but in the shielded case we can’t encode all imaginable options of hashes, and passing the circuit as input doesn’t seem to be viable at this point

1 Like
8

They are proving different things (deltas for different resources / combinations of resources), and might have different proving systems. No other differences as I understand this (@xuyang might have a more specific picture).

Makes sense. If it’s necessary, we could also perhaps just insist on a standard delta proof format.

My idea is that these would need to be explicitly allowed by the resource logic.

We would use multihashes in this hypothetical (maybe we should use them anyways) - but different proof systems in the same action doesn’t add any expressive capacity that we don’t already have, as far as I can see, so I think it’s OK not to support that for now. We should think about, however, whether this will entail extra complexity for developers (but we should go ahead in the meantime).

9

Okay, then I don’t understand how it would solve the delta problem

Or we can also only allow RMs that use the same delta proving system in the same tx

But when we are composing transactions of two different RMs, we presumably do it to achieve balance or valid rl proofs. At the same time, if RMs use different hashes for kinds and we treat these kinds differently, then the balance becomes only logic-checkable property (we would have dummy resources for delta balance and check the “real” balance in the logic, where we can tell what kinds are equivalent). In that case, both txs being composed are strictly speaking balanced, but not valid because the logics are not satisfied. At the same time, to have the logic that checks the cross-kind balance satisfied, we need the resources of these two different RMs in the same action - something we decided to prohibit for now. Then what is the usecase for composing transactions of different RMs?

1 Like
10

The proposed solution for balancing resources of different RMs in the same transaction

The need for having resources of different RMs in the same transaction is desired to allow either balancing a single transaction with resources of different RMs (1) or ensuring transaction validity (logic proofs) with resources of different RMs (2) or both.

1. Balancing resources of different RMs (delta proof)

To ensure delta interoperability across different RMs in the same transaction, we need the primitives and the inputs to be the same to have the deltas compatible. The relevant inputs are:

  • logic
  • label
  • quantity

The relevant primitives are:

  • LogicHash
  • LogicHashRef
  • LabelHash
  • KindHash
  • DeltaHash
  • DeltaProvingSystem

Having the same inputs is required by definition of kind/delta. But having all of the primitives being fixed is quite limiting. We can relax this requirement by not requiring the exact same sets of primitives for both RMs (assuming there are two), but having the primitives compatible with both RMs and verifying balances explicitly in resource logics. In this case, the transaction delta would balance artificially with dummy resources - each RM side would create dummy resources required for the balance.

Q: do logics have to explicitly encode this case? The logics have to know if they should expect the “same RM resources balance” case and outsource the balance computation to the delta proof (how it is usually done), or “different RM resource balance” case and check the kinds itself? Should it always be possible (and therefore always be included in the logic code), or is it a special case the logics have to explicitly allow?

This reduces the delta case to the logic validity case.

2. Ensuring transaction validity with resources of different RMs

This case implies that now the logics are responsible for the balance check, which in turn implies:

  1. the resources of different RMs have to be in the same action (to be in the same proving scope)
  2. logics have to know how to validate resource objects produced by different RMs

The proposed solution to allow (2) is to introduce multiformats for the primitives relevant to the checks required in logics to validate resources of different RMs.

Multiformats wouldn’t help with delta proofs because it would make them verifiable, but wouldn’t solve the composability issue

To validate the resource object, the logic need to know how to:

  1. compute resource tag from the resource object → commitment / nullifier hashes are multihashes

To perform the balance check, the logic need to be make sure that the resources have the same “conceptual” kind:

  • LabelHash, LogicHash, LogicHashRef - multihashes

After verifying that labels and logics are what they are expected to be, we can check the balance on the quantities directly (quantities have to be compatible too).

Using multiformats allows the RMs to have higher compatibility chances. In that case, the logic would have to know how to compute hashes of different types, which in shielded case can be not very nice, but we accept that.

TL; DR

  • allow different RM resources to be in the same action (but not compliance unit)
  • verify balance across RMs in logics
  • use multiformats to increase the chances that both RMs can recognise the primitives used by each other

Leftovers: ways to have kind independent of the proving system representation of the logic

  1. have the logic to contain multiple versions of the same algorithm written for different backends. Requires some duplication of data + adding a new proving system to the bundle is not possible without updating the kind
  2. have a universal logic representation that can be compiled to any proving system - in that case the proving system is abstracted away from the kind computation. Verification would require the user to compile the logic to the backend circuit or somehow verify the correspondence of the circuit the prover used and the universal circuit representation

Let me know if I forgot something @cwgoes @xuyang @alberto

1 Like
11

I’m trying to understand the details in practice. I’m still a little confused. The resource logic can only access the current execution context(action scope). Could someone please explain how balance verification works in the resource logic, and whether it occurs in every logic or just specific ones?

Q: do logics have to explicitly encode this case?

I have the same question.
Regarding dummy resources, the rights and cases should be explicitly defined in the resource logic to allow for the creation of dummy resources with a true ephemeral flag, like we are using in special scenarios involving resource minting and destroying transactions(btw, is it documented in the application spec?). Otherwise, it could be risky to permit the creation of dummy resources (of the same kind but with a true ephemeral flag) for general purposes. We might be cautious about this kind of dummy resource creation.

12

I’ll give you an example: imagine we have a transaction with a created resource of kind1 and quantity 1, consumed resource of kind2 and quantity 1, and one created and one consumed resource of quantity 1 and kind3. Imagine we want kind1 be considered equivalent to kind2. We can’t do that in the delta proof, so we have to:

  1. add two dummy resources: a consumed resource of kind1 and a created resource of kind2 to artificially balance delta for these kinds
  2. put the resources of kind1 and kind2 in the same action
  3. both logics of these resources would have to check that:
    1. the resources in the scope have kind1 or kind2 (if there are also resources of other kinds in the action, they still need to be checked, but they irrelevant for the balance check)
    2. the non-dummy created resources of kind1/kind2 balance non-dummy consumed resources of kind1/kind2
    3. (dummy resources we created for delta balance should also be validated, but it is important to make sure that in logics we check the balance for non-dummy resources)
  4. For the resource of kind3, the balance works the usual way. Delta sees a consumed resource of kind3, a created resource of kind3, and checks that the quantities are equal
13

Yeah I agree, all dummy/ephemeral resource creations should be explicitly validated in logics and only allowed for certain purposes, and otherwise not allowed

Essentially such resources allow us to customise the default mechanisms, and this should only be allowed in certain cases

1 Like
14

Thanks for the explanation

In practice, the normal created resource of kind1 and consumed resource of kind2 can be constructed by different actors in separate actions.

I’m wondering if we could combine logic and delta to make it work based on your solution.
And in step one and two, add and put the dummy resources of kind1 and kind2 in the same action, which can be completed by any actors, including a solver. Then in 3.2,

  1. the non-dummy created resources of kind1/kind2 balance non-dummy consumed resources of kind1/kind2

Instead, we check the dummy consumed resource of kind1 and the dummy created resource of kind2 are balanced realistically but not physically, to make sure the dummy resources don’t introduce unbalance risk. Ultimately, the delta of kind1 and kind2 works as usual.

I’m concerned that it might complicate the resource logic. We need to include various dummy cases in the logic, explain the mechanism to application developers, and ensure their compliance. Besides, even though kind1 logic may skip “balance” checking without interoperability requirements, we still have to pass a padding kind2 resource to kind1 logic each time.

There might be an extensible issue. When a new RM is constructed, the new kind (e.g., “kind_new”) could be considered equivalent to kind1 and kind2. We may need to adjust the logic for better interoperability with kind_new. However, if the logic is changed, all kinds will also change.

If we can assume that kind1 can be considered equivalent to kind2, when they are in different resource RMs. I’m considering perhaps we could utilize the same conversion technique(circuit) employed in MASP

1 Like
15

If they are in different actions, we can use ephemeral resources to carry the balance condition: a resource of kind1 is in the first action with a created intent resource saying that this intent resource can only be consumed if another resource of kind2 with quantity equal to resource of the kind1 is a part of the other action. This way the balance is ensured not in the kind1/kind2 logics and can also be checked across actions

1 Like