anoma / green

https://anoma.github.io/anoma/
MIT License
7 stars 0 forks source link

Resource logic inputs are not in line with the specs #711

Closed heueristik closed 1 month ago

heueristik commented 3 months ago

customer: @heueristik performer: deadline: estimated: started: actual: completed: confirmed: dependencies:

supersedes:


The resource logic inputs are not in line with the RM specs, which poses a problem for some applications.

In particular, resource logic functions need the $tag$ argument (which is either the $cm$ or $nf$ depending on if the associated resource is created or consumed -- ask @vveiln for more details) to be able to use the nullifier associated with a resource, e.g., as a lookup key in the extra data (see the applications ART, e.g., here or here for more context).

XuyangSong commented 2 months ago

The design is assumed to be from the Taiga protocol. Essentially, we only need the tag as the logic output to indicate the owner of the resource logic. For instance, in a single transaction, there may be multiple resources with the same resource logic. The outputted tags are necessary to record and ensure that each specific logic of the resources is executed.

The owner tag can be passed, and the owner resource can be searched by the tag in the corresponding logic, returning the tag in the end. This is a common practice in Taiga application examples. However, there are other options available as well. For instance, we can fix the order of resources for the logic when passing them to it. If we designate the first (or any other position) resource as the owner, there would be no need for an extra tag argument. Nevertheless, outputting the tag should still be mandatory for shielded cases.

As we have access to all the plaintext resources in transparent cases, the tag in the logic result may not be necessary? We might already have mechanisms to ensure correct execution of all logics? @juped would be best to answer it.

cc @mariari

heueristik commented 2 months ago

On the Juvix side, the input arguments for resource logic functions are

logic (self : Resource) (tx : Transaction) : Bool :=
...

which I cannot fully map to

Resource Logic Public Inputs:

  • $nfs \subset nfs_{tx}$
  • $cms \subset cms_{tx}$
  • custom inputs

Resource Logic Private Inputs:

  • input resources corresponding to the elements of $nfs$
  • output resource corresponding to the elements of $cms$
  • $tag: \mathbb{F}_{tag}$ — identifies the resources being checked
  • custom inputs

in the transparent case. In particular, we seem to lack the "identifies the resources being checked" part. In taiga as also @vveiln writes, there apparently is the $tag$ mechanism to identify the commitment or the nullifier of the resource.

As we have access to all the plaintext resources in transparent cases, the tag in the logic result may not be necessary?

In the transparent case, I cannot associate resource plaintexts with nullifiers inside the resource logic currently. I only have the resource plaintexts, here named self, from which I can only compute $cm$ inside the resource logic but not $nf$ because the nullifier key $nk$ is not known there (we certainly don't want to put $nk$ into the $extra$ data of the transaction). This is what this issue is about.

See also the related thread opened by @degregat

heueristik commented 2 months ago

After a meeting with @XuyangSong @mariari, we agreed that providing the $tag$ as a resource logic function input is a solution to the problem that I encountered and would be in line with the RM specs.

Note that the general correspondence between nullifiers and resources is an open discussion in the forum.

XuyangSong commented 2 months ago

After a meeting with @XuyangSong @mariari, we agreed that providing the tag as a resource logic function input is a solution to the problem that I encountered and would be in line with the RM specs.

Note that the general correspondence between nullifiers and resources is an open discussion in the forum.

wait, in my opinion the reference from forum should be correct, which is actually I described above.

Resource Logic Public Inputs:

  • $nfs \subset nfs_{tx}$
  • $cms \subset cms_{tx}$
  • $tag: \mathbb{F}_{tag}$ — identifies the resources being checked
  • $extra \subset tx.extra$

Resource Logic Private Inputs:

  • input resources corresponding to the elements of $nfs$
  • output resource corresponding to the elements of $cms$
  • custom inputs

The tag should be in the Public Inputs instead of the Private Inputs.

XuyangSong commented 2 months ago

@heueristik The issue would be solved if we add the tag to transparent Public inputs because transparent logics can access them.

XuyangSong commented 2 months ago

Another problem in transparent cases might be that we pass all the required resources (Resource.ProofRecord) along with public inputs to the resource logic, but we don't have the custom inputs argument. So sometimes they have to put the custom inputs into extra, which seems weird but it actually works. Because private and public data don't make any difference for transparent logic. Am I understanding correctly? @juped

heueristik commented 2 months ago

So sometimes they have to put the custom inputs into extra, which seems weird but it actually works

Yes, this is also confusing. I assume that @vveiln had a reason for having private custom inputs and public extra data. This is what I could find in the specs:

The party responsible for creating proofs is also responsible for providing the input to the proving system. Public inputs are required to verify the proof and must be available to any party that verifies the proof; private inputs do not have to be available and can be stored locally by the proof creator. The same rule applies to custom (inputs not specified by the ARM) public and private inputs.

A concrete implementation of the ARM can specify more mandatory inputs and checks (e.g., if the resources are distributed in-band, resource logics have to check that the distributed encrypted value indeed encrypts the resources creat- ed/consumed in the transaction), but the option ofcustom inputs and constraints must be supported to enable different resource logic instances existing on the application level.

Putting information into extra data that everyone can see and mutate (extra data is mutable, e.g., by solvers or gossiping nodes) might have security implications.

I would like to have an example of what a private custom input could be (in the transparent and shielded case) myself.

heueristik commented 2 months ago

Oh, I just realized that the current version of the report found here https://zenodo.org/records/10689620 has it as a public input, whereas the one on Github that I kept quoting is outdated.

Bildschirmfoto 2024-07-26 um 09 51 02

Can you please update the one on GH as well @vveiln ?

heueristik commented 2 months ago

wait, in my opinion the reference from forum should be correct, which is actually I described above.

Now I get what you meant by that.

heueristik commented 1 month ago

Apps will be written against the general RM interface as specified in https://github.com/anoma/juvix-arm-specs. This will supersede this issue