Resource logics: Connecting nullifiers and consumed resources

Thanks, this is helpful to refresh my memory. My understanding from this document is that the one and only reason we need a nullifier key is to ensure that the creator of a resource cannot see when it is spent (nullified) - is that correct? I think that’s a point in support of the approach of treating the nullifier key as a detail that must be dealt with when creating a shielded resource (future spends of which one does not want to be detectable by the sender), but that otherwise should carry no meaningful application semantics.

2 Likes

Minor detail: nullifier key exists to address the created resource to the receiver (whose key is used to nullify the resource being created?), nullifier public key exists to hide the fact of consuming the resource from the creator of the resource. But I fully agree with you about treating nullifier keys as an implementation detail only meaningful for the shielded case.

2 Likes

It is convenient for application development to just put the ExternalIdentity/public key of the receiver as the nullifierKeyCommitment. However, this entails that the nullifierKey is the InternalIdentity / private key, which is sensitive information and should never be shared.

To connect nullifiers and consumed resources, I realized I don’t need to share nullifier keys because I can simply provide a mapping Map Nullifier Resource in the custom inputs.
This should work fine for now, but still is a bit clunky and seems to be a repeated pattern required for almost every app (most resource logics want to look up, e.g., the resource behind the Nullifier from the Tag argument to check app-specific constraints, e.g., on the Label or Data fields).
For convenience, I’ve also put a mapping Map Commitment Resource in the custom inputs, so that I don’t need to recompute commitments to find corresponding resources. Overall, this leads to some resource logic code duplication.

This could potentially be optimized (since this repeated information also increases transaction sizes unnecessarily) by requiring ordered sets so that PublicInputs.commitments and PublicInputs.nullifiers have the same order as PrivateInputs.created and PrivateInputs.consumed, respectively.
There is a trade-off because this ordering would then need to be enforced as part of the compliance proof, which could also be costly.

1 Like

I want to clarify here: by “custom inputs” do you mean “private inputs” (or generally the inputs which are not checked against other data in the transaction)? I may be using out-of-date terminology here, but wanted to be sure (and if not, we should standardize this terminology).

I think that is alright as a design pattern at an architectural level, but I agree that it would be annoying for developers to do every time, and this is a good example of something that should be abstracted by a standard library and/or some higher-order functions. For example, we could have a “magic” function that looks up a resource by nullifier (or similarly for commitment), and if that function is used, we pull in the right data to the custom inputs automatically, but if not we have no need to. This might indicate the need for some kind of “resource logic monad” which makes these capabilities available. I’m not quite sure of the best implementation method here, maybe @paulcadman would have some ideas.

Does this ordering really need to be enforced as part of the compliance proof? Can’t we just assume the sets are ordered, and let the resource logic fail if they aren’t?

1 Like

Yes, I mean the custom inputs being part of the logic function private inputs (see here Resource logic - Anoma Specification).
In juvix-arm-specs, we defined them as follows:

  --- Custom inputs of the resource logic function proof being defined on the application level.
  --- TODO To support the definition of ;CustomInputs; on the application level, Juvix must support existential types.
  --- NOTE: For the private testnet, this can be of type ;AppData;.
  type CustomInputs := mkCustomInputs@{unCustomInputs : MISSING_DEFINITION};

  --- The private inputs (Witness) of the resource logic function proof.
  type Witness :=
    mkWitness@{
      created : Set Resource;
      consumed : Set Resource;
      customInputs : CustomInputs
    };

(juvix-arm-specs/Anoma/Proving/Types.juvix at 3d04a1231847df4d3d2b4a0d37a454e96404bab0 · anoma/juvix-arm-specs · GitHub)

1 Like

Hmm, I have to think about it because it could have security implications.

Yes, I was also thinking about it, but I think it does not, as long as there is no case such that:

  • a set passed unordered causes the resource logic to pass, where
  • that same set passed ordered would cause the resource logic to fail, for
  • a resource logic that is otherwise sensible

Certainly one could write a resource logic which violates the condition, but it would not be “treating” this input as an ordered set in the sense which I think we mean here. This may still be preferable to avoid just because it might be confusing, though…