Yulia/app data update

[vveiln]

This PR adds the following changes to the spec:

• a new proposed applicationData structure with four reserved fields: resourcePayload, discoveryPayload, externalPayload, and logicVKOuter hash.
• replaces the previous logicVKOuter field in logicVerifierInputs with a generic verifyingKey and moves logicVKOuter to appData, as described above
• removes the isConsumed flag from logicVerifierInputs as in can be inferred from the compliance instance structure

⚠️ The scope of this PR is the three changes described above. All other requested changes are out of the scope ⚠️

All relevant changes are in this file: docs/arch/system/state/resource_machine/data_structures/action/index.juvix.md (everything else is some random stuff git made me do)

[github-actions]

The preview of this PR has been deleted.

[XuyangSong]

lgtm
Left a comment regarding the commitment to logicRef in logicVKOuter.

[XuyangSong]

Are you using logicVKOuter to unify the inner logic instance in DP with the outer instance in FP? In FP, it would be better to use a hiding and binding commitment to verifyingKey, which implicitly includes logicRef = hash(verifyingKey) — specifically, cm = commit(hash(verifyingKey), r). Alternatively, we can add the hash check explicitly. Since we can also retrieve logicRef from the inner instance's logicVKOuter in the outer circuit, we still need the hash check because the inner logicRef is not reliable for outer circuits. It could be ambiguous where the logicRef comes from if only a commitment to logicRef is provided.

In FP compliance, we commit to logicRef without requiring a hash.

[vveiln]

logicVKOuter corresponds to logicRef in the DP case (the one we pass to compliance to check against r.logicRef) and to a proper commitment in FP case. verifyingKey contains the actual field to be used to verify the proof

My impression is that it is just like we discussed it, but without the extra FP details (they will go to the risc0 spec)

[agureev]

Minor thought in addition: what if the type of appdata will instead be:

Map(payload => List(Bitsring, DeletionCriterion))

where payload can be any of some encoding of strings resourcePayload, discoveryPayload, externalCallPayload, logicVKOuter, appPayload

That way "empty field" comment would make sense to me as that would mean that the key would just have an empty list attached.

We can then just decide which payload goes in which order for the circuit to process.

[agureev]

What does "field left empty" mean? The datatype of appdata is a List(Bitstring, DeletionCriterion). I am unsure what the notion of "field" is here and what does "empty" mean here.

[agureev]

Can you also elaborate on what "resource-object-related-data" is?

[vveiln]

You are right, it shouldn't be just empty. It should be some reserved bitstring sequence that basically means empty.

Resource-oject-related data is any data about the resource object that is required to be passed. In the shielded case it would be the encrypted resource object. It could also be resource object itself, without encryption.

[agureev]

Similar here re "field empty".

[agureev]

Similar here re "field empty".

[agureev]

Can you elaborate how that relates to the logicVKOuter in the Compliance Units?

Is it something extra to be checked in the verify?

[vveiln]

logicVKOuter is passed as input to the compliance proof to verify it is correctly computed from logicRef. It is the same field here and there. In the data privacy case (our only case currently), it is only used in compliance proof check. In the FP case, it would be passed as input to the outer circuit as well. Do you think it makes more sense to just keep it in compliance instance and get it from there for FP case?

[agureev]

@XuyangSong would probably know better here

I think the only thing I can say is my general rule of thumb is: do not duplicate information when unneeded as that just introduces extra checks to make.

E.g. adding this to appdata instead of asking the verifier to put the corresponding logicVKOuter from the Compliance Units means that we either way need to search for it and make sure it corresponds.

Similarly to isConsumed, where we need to explicitly make sure that the tag appears in the correct position in the compliance unit to make sure all the semantics get satisfied.

Hopefully this makes sense.

[vveiln]

I'll remove it

[XuyangSong]

Minor thought in addition: what if the type of appdata will instead be:

Map(payload => List(Bitsring, DeletionCriterion))

where payload can be any of some encoding of strings resourcePayload, discoveryPayload, externalCallPayload, logicVKOuter, appPayload

That way "empty field" comment would make sense to me as that would mean that the key would just have an empty list attached.

We can then just decide which payload goes in which order for the circuit to process.

I agree that a map should be clearer. Let’s first check if it’s costly in circuits and Solidity. I’ll run some circuit tests. I believe @heueristik can confirm the cost in Solidity.

[agureev]

I agree that a map should be clearer. Let’s first check if it’s costly in circuits and Solidity. I’ll run some circuit tests. I believe @heueristik can confirm the cost in Solidity.

The "maps" we use in solidity are just a list of 2-tuples, so should be fine.

[vveiln]

Minor thought in addition: what if the type of appdata will instead be:

Map(payload => List(Bitsring, DeletionCriterion))

where payload can be any of some encoding of strings resourcePayload, discoveryPayload, externalCallPayload, logicVKOuter, appPayload

That way "empty field" comment would make sense to me as that would mean that the key would just have an empty list attached.

We can then just decide which payload goes in which order for the circuit to process.

That makes sense as a solution to the problem, but wouldn't it be just easier to define an "empty" bitstring sequence that for the reserved fields mean that they are empty instead of layering the data structure?

[XuyangSong]

I agree that a map should be clearer. Let’s first check if it’s costly in circuits and Solidity. I’ll run some circuit tests. I believe @heueristik can confirm the cost in Solidity.

The "maps" we use in solidity are just a list of 2-tuples, so should be fine.

I mean the operations in the map, like get, insert, etc.
n rust/c++ standard lib, a map usually refers to a HashMap. If you mean the trivial tuple with key and value, I think that's fine. In rust, we would use vec<(k, v)>

[agureev]

That makes sense as a solution to the problem, but wouldn't it be just easier to define an "empty" bitstring sequence that for the reserved fields mean that they are empty instead of layering the data structure?

I think that both things can be solutions to the problem. It would be a matter of practical utility. I would say that the proposal to make it a map with values being lists is twofold:

1. That way application circuits to not have to be explicitly aware of any additional arguments, e.g. the trivial logic previously did not need anything in appdata to generate proofs, now it has all these empty hashes fed to it inside the circuit.

2. This allows more general encoding of payloads, e.g. for the forwarder calls the externalCallPayload requires containing several data: e.g. the forwarder call, inputs to it, outputs to it, the resource plaintext, the nullifier key. In the proposal to put it into a fixed position, we are saying that we need to encode it all into one bitstring. We can of course do that. But a simpler way would be to encode it as separate items of a list. For Solidity it is actually great because try scenarios are hard to use and we may have two different datatypes that we are looking for decoding if we put it all into one position: either (ForwardCallData, Resource) or (ForwardCallData, Resource, NFKey)

So in my proposal to make it a map we can instead just put externalCallPayload => [forwardCallBlob, ResourceBlob] if the resource is created and externalCallPayload => [forwardCallBlob, ResourceBlob, NFKeyBlob] if consumed.

Well, the point I guess I am trying to make is that this way the individual RMs can figure out how to put data there with greater ease.

How does that sound @XuyangSong @vveiln

[vveiln]

That way application circuits to not have to be explicitly aware of any additional arguments, e.g. the trivial logic previously did not need anything in appdata to generate proofs, now it has all these empty hashes fed to it inside the circuit.

The verifier would know that an empty hash is an empty parameter and just wouldn't pass it to the logic, the logic wouldn't have to see these inputs.

I agree with the encoding point though, it also would offload the work from the circuit, which is always good.

I'll change the format to the proposed one.

[agureev]

@vveiln another idea I just had is maybe just make it a 5-tuple of lists? So the type would be {List(BlobWIthDelCriterion), List(BlobWIthDelCriterion), List(BlobWIthDelCriterion), List(BlobWIthDelCriterion), List(BlobWIthDelCriterion)}

Where each position is beforehand tied to one of the payloads?

That way we don't have to worry about how to encode names of the fields and beforehand decide on the order all of this goes in to the instance

[vveiln]

I removed logicVKOuter from applicationData and changed applicationData type to:

(
  [(BitString, DC), ..] #resourcePayload
  [(BitString, DC), ..] #discoveryPayload
  [(BitString, DC), ..] #externalPayload
  [(BitString, DC), ..] #applicationPayload
)

[jonaprieto]

Why are you deleting all those files? See the files changed

[vveiln]

These changes were generated by git automatically. As I understand, this is the diff between main and v1.0.0 – all the files related to engines and such removed, but I might be wrong.

[XuyangSong]

I removed logicVKOuter from applicationData and changed applicationData type to:

(
  [(BitString, DC), ..] #resourcePayload
  [(BitString, DC), ..] #discoveryPayload
  [(BitString, DC), ..] #externalPayload
  [(BitString, DC), ..] #applicationPayload
)

Are we using a fixed array here? The struct would look like this:

struct AppData ( [Vec<(Vec<u8>, DC)>; 4] )

If only four entries are involved, do you think we can add the payload names to the struct? It seems better than relying on fixed positions. such as

struct AppData {
    resource_payload: Vec<(Vec<u8>, DC)>,
    discovery_payload: Vec<(Vec<u8>, DC)>,
    external_payload: Vec<(Vec<u8>, DC)>,
    application_payload: Vec<(Vec<u8>, DC)>,
}

If we plan to extend payloads to five or six in the future, the fixed array may not be suitable, and we can use a variable array instead, like:

struct AppData (Vec<Vec<(Vec<u8>, DC)>>)

Then developers need to remember the positions.

@vveiln @agureev
Let me know your preference.

[agureev]

If only four entries are involved, do you think we can add the payload names to the struct?

I think this can be seen as an implementation detail. The struct you have can have the same semantics as the 4-tuple. Either way we have to order them in some way in order to know in which order to place them into the instance.

In other words, I think we can make the appdata the struct you mentioned without needing to change the current spec. So I am ambivalent as to whether we change it to an ADT or just keep it like a tuple.

But I actually would also like for the implementation to be a stuct on the Rust/Solidity side.

[agureev]

Sorry for vetoing the upgrade again, but I am unsure why we are putting the depth in the Action datatype. Could you elaborate on that?

Also, do we need to change anything for the Compliance Unit? It would be really nice if the compliance unit could accept variable-size commitment-accumulator.

[agureev]

Should this be part of the action? Why do we need to let the user provide it?

Wouldn't it be the RM that decides beforehand whether it will use the smallest action tree needed or a fixed-size one based on the proving system it uses?

[vveiln]

Because we want the verifier to know the depth of the tree to build in case the depth is not set dynamically. It is added for compatibility with proving systems that do not support variable tree size like zkvms do.

[agureev]

I have to think about that.

But also: what is the type of the input and what do we mean by "empty"?

Maybe we can decide on a type of integers and if the value is -1 we construct the least size one?

Or maybe we can just make it natural numbers? i.e. not include the option for it to be "empty"?

That way it's the higher-level interface which will compute that number if needed.

[agureev]

I do think I now understand the usefulness of this for RMs that have proving systems that can only have fixed-size argments and hence support only fixed-size merkle proofs.

This way it's the application developer who decides how many resources can exist with the resource in the same action instead of us. E.g. currently we support only 16 resources per action, it is a cutoff based on the RM design as that's the tree which we construct

But now you submit the tree depth information yourself and hence determine the proof length that you expect

However, that does mean only apps which expect the same depth can be part of the same action

So every application can have different verifying keys based on which tree depth they expect

I dunno how much we would want that...

But for the veritable tree depth supporting proving systems, how does it help? I am unsure still

[agureev]

Outside of this PR but wanted to mention:

At some point we should probably change this page to reflect the part that we don't control the witness of the resource logics.

Moreover, parts 3 and 4 seem to imply that we put all the resources created and consumed into the witness info. However as we have discussed this actually rarely happens and we don't even have apps that have such witness structure.

[vveiln]

At some point we should probably change this page to reflect the part that we don't control the witness of the resource logics.

I'm not sure what you mean by that. We generally can't control anything that is provided by the user, but we specify what we expect to receive

Moreover, parts 3 and 4 seem to imply that we put all the resources created and consumed into the witness info. However as we have discussed this actually rarely happens and we don't even have apps that have such witness structure.

I'll add a note that passing all resource objects as witnesses is not necessary, but we can't say if it happens rarely in principle