Input argument types of the compliance proof `prove` function

Resource Machine Stuff
1

In a chat with @vveiln about compliance proofs, she said the following:

Compliance proofs are computed by whoever creates the action

For now, let’s assume a simple token transfer transaction (with one action) that is balanced already and doesn’t require solving. In this case a user, by calling some transfer transaction function, computes the compliance proof(s) locally.

This means that the transfer transaction function needs to call the prove function below.

However, in the last engineering office hours, @paulcadman and I were told that the Compliance.Instance and Compliance.Witness types in the compliance proving system are UNUSED.

How can we resolve this? Did I understand something wrongly during the office hours @ray?

Ping @mariari for visibility.

2

I just talked to @ray and @mariari during the skunks office hours again. It’s indeed the case that I currently don’t need to provide input arguments to the compliance proving system prove function. The transparent resource machine discards those and just puts the string “compliance” in for the Compliance.Instance and Compliance.Witness arguments.

Moreover, I was told that the transparent RM takes all the information it needs for the existence checks (that are required for the compliance proof computation) from the resource logic proving inputs (I assume ResourceLogic.Instance and ResourceLogic.Witness). Please correct me if I am relaying this information wrongly.

Personally, I just need to know what information transaction functions need in order to populate the compliance proofs (besides resource logic proofs) in the Action.proofs field.
If you, @vveiln, could let me know if this is ok, I can move on.

3

Well you put them there, but they effectively get tossed, as we do offer functions that generate these.

4

I still need to know what I should formally put there, even if it gets discarded, to make it transparent/explicit to people using it. @vveiln can tell me. Please help her and me by translating it into Juvix data types.

The reasoning is that these functions/apps could theoretically also be used with the shielded RM (although this is not relevant for the testnet yet). If I have to provide something that is not straightforward to obtain and this would require me to refactor the applications because of this, that could cause me troubles. That’s why I am trying to prevent this.

Ultimately, apps must be written for the general interface and not for specific instantiations.

5

You can send in any type you want.

prove
  (provingKey : Compliance.ProvingKey)
  (publicInputs : Compliance.Instance)
  (privateInputs : Compliance.Witness)
  : Compliance.Proof := STILL_MISSING_ANOMA_BUILTIN;

works, you can make the signature however you see fit, the nock code handles whatever you want here!

6

I understood this. Still, see my explanation above

7

I don’t understand, where does it get the arguments for proving?

Moreover, I was told that the transparent RM takes all the information it needs for the existence checks (that are required for the compliance proof computation) from the resource logic proving inputs (I assume ResourceLogic.Instance and ResourceLogic.Witness ).

This makes no sense since different logics have different inputs and compliance circuit has the same expected inputs. If the logic inputs are somehow parsed and only the relevant parameters are taken, it is still wrong because it doesn’t correspond to the spec.

We need the transparent RM work in the way that anyone who reads the spec without being familiar with the RM code can verify a transparent RM transaction. Can we parse the arguments earlier and put them in Compliance.Instance and Compliance.Witness as well as the RL Instance and Witness fields?

Personally, I just need to know what information transaction functions need in order to populate the compliance proofs (besides resource logic proofs) in the Action.proofs field.

I cannot give you the exact parameters you need to compute compliance proofs because it depends on the instantiation choices for different functions. You can get some guidance from the checks the compliance circuit must perform: Action - Anoma Specification

Ultimately, apps must be written for the general interface and not for specific instantiations.

I think it is only possible to a degree, because the way you compute e.g. nullifiers differs between different instantiations, and your application logics must check correct derivation of nullifiers, which means that these parts of the application has to be adjusted for specific RM instantiations. It is similar with some other parameter computations, including the compliance circuit

1 Like
8

Why is this not possible? The RM interface defines types and functions that an RM instantiator can define and implement. If applications only use the functions and types from this interface, then they don’t need to care about the concrete implementation. This of course means that the interface function signatures aren’t allowed to change between RM instantiations.

I see no problem in, e.g., different nullifier derivation and check implementations between RM instantiations. Ultimately, these are functions that create and verify nullifiers, which I can call.

1 Like
9

Ah yes, if these functions are provided by the instantiation, then sure. I was thinking about writing self-contained logics

2 Likes
10

Since I was asked: The prove function signature is specified here: Proof - Anoma Specification.

This makes no sense since different logics have different inputs and compliance circuit has the same expected inputs. If the logic inputs are somehow parsed and only the relevant parameters are taken, it is still wrong because it doesn’t correspond to the spec.

What needs to happen now?

11

I’m not sure I understand the question (if it was for me)