Report on QTT-RM Ideation

[ArtemG]

This post and ideation has been prompted by a discussion made during the planning of the cryptography team Dagon work as documented in this post. In particular, the proposal to move the Resource Machine to the ideation phase for some time in order to see whether we can improve its design.

I here present a subjective 3-point list of reasons which I think make it worth re-ideating the RM:

1. It’s hard to formulate properties regarding the resource machine
2. It is hard to explain the resource machine to third-parties and even internal parties without them being heavily engaged
3. It is hard to write applications for the resource machine

Points 1 and 2 make it also hard to extend the RM to actually support projects important for Anoma such as Controllers. Take, e.g. a comment by @isheff:

I’ve always hated balance. I never understood why we needed it if we already allow resource logic to encode arbitrary predicates over resources created and consumed.

This is not to say here that balance is somehow ill-used, but that the design choices are obscured and hence make it hard to extend to our needs as there seems to be no principled or “correct” ways of doing it. Nevertheless, we are looking to make major changes soon.

In particular, I consider the decisions made on the ideation of the RM to be the main blocker for further Dagon development - seemingly all Dagon sub-projects touch upon the RM in some sense.

Due to this, I wanted to - per @mariari 's request before Hacker House starts - present a preliminary report on a personal ideation on the RM design and possible resolutions to 1-3 through trying to make an RM into a model of Quantitative Type Theory, or more precisely to a model of a QTT over a semiring of natural numbers tagged by whether the usage is affine or linear.

The point of the report is to start active conversation on ideation and present with a sort of reasoning that might be useful to some folks in the organization to do ideations of their own into the topic. This is not a formal proposal. This piece is simply a conversation starter that hopefully will lead to a proper proposal.

This thread I will split into four parts:

• Ideation Setup
• Ideation
• Ideation with Concrete Changes
• Conclusion

The setup part will deal with some of the presuppositions of why this specific ideation took place (rather than e.g. ideating on some other connections) and what are the criteria for the success of the project.

The core ideation part will talk about what an RM modelling a QTT may look like.

The third post will try to spell-out some concrete changes which may be made to make the model a reality.

The conclusion is a general reflection on ideation, which things worked and which did not.

[ArtemG]

Ideation Setup

So we start with trying to deal with problems 1-3 listed above.

1 and 2 seem to be solvable by recognizing the RM as a model of some mathematical theory. The more studied the mathematical theory chosen the better as these will already have a lot of properties proven which may map to the RM. The easier it is to recognize the RM as a model of said theory the better as that will contribute to point 2.

So here I take for granted that what we ultimately want is to understand the mathematical theory behind the RM.

Point 3 then would encourage us to - given our current endeavors regarding object-compilation - to pursue such a mathematical theory that it has as much computational content as possible.

This brought me to

Type Theory

Type theory evidently satisfies both of the criteria. Moreover, if I recall correctly, in our RM designs we have been inspired by these topics already:

• the term^[1] “resource” we borrow from linear logic/TT
• “quantity” was - at least as was told to me - inspired by Quantitative Type Theory (QTT)

Here it is important to talk a bit about QTT. Quantitative type theory - roughly - is a type theory where terms carry some “computational” information about how many times said term can be used in a derivation.

In case anyone is interested, a paper that I found insightful is Counting on QTT.

The nice example that paper uses is:

1 x : Bool, 1 y : Nat, 0 z : Nat \vdash if x then y + 1 else y + 2 : Nat

which corresponds to the fact that we can use x boolean exactly once, y natural number exactly once and z never inside the derivation (or runtime, whatever term you prefer better to feed your intuition). Basically, we provide exact information about how much can you use a specific variable during execution of some program.

Quantitative type theory usually is presented over some semiring. The case that would interest us is the semiring Nat. Another semiring that we may get interested in is the semiring

\{(n, type) \colon Nat \times \{\text{Linear, Affine\}\}}

where if a variable is annotated by (n, Linear) it is interpreted as saying that the variable can be used exactly n times while (n, Affine) is a variable that can be used at most n times in a single runtime/derivation. The summation/multiplication is given as a product on the same operations over Nat and Linear + Linear = Linear, Affine + Affine = Affine, Linear + Affine = Affine.

Looking at this sometimes it seems like some parallels with the RM as it is currently designed pops out: resources as terms, kinds as types, a single transaction is like a derivation/runtime, and delta is tracking the use of variables, etc…

However the analogy breaks quite quickly sadly. The last time we discussed this we uniformly agreed that the current RM design diverges from the analogy by the sole fact that delta tracks the usage of types, not of terms. In QTT what is anotated are terms - as in Resources - and not types - as in kinds. However delta makes sure that the kinds are balanced, not the terms. To quote @cwgoes :

@cwgoes

Yes, I think you are right that the current system does not correspond as closely to QTT as the one you’re proposing – at the moment, the quantities are of types in a certain sense, in the sense that you can combine the quantities of different terms of the same type, and the linearity check “forgets” that the terms were different.

Nevertheless, I tried to return to the idea of researching how would an RM corresponding to a QTT look like because I honestly do not think there is too much (sic) to do to make it work. Some correspondences were already-always present and its up to us to make them precise.

And if we do, then I think that this will resolve 1-2 instantly. People have been talking about type theories in some form for more than a century now and QTT also has had quite a few developments.

Problem 3 then would get resolved by the Curry-Howard isomorphism. Well, of course it’s not that simple, but nevertheless, it would be fundamentally easier to get a computational interpretation using a framework that has historically been associated with computational interpretations.

The Resource Machine

However before diving into the changes and correspondences this research has proposed for the resource machine design, it is good to set some base grounds.

The amazing thing about the RM design as it is now is that it works. Moreover, it works great! It is a working architecture for supporting arbitrary shielded applications. This is an amazing feat as-is. Changing the design non-conservatively - i.e. not preserving some of the core features - is pointless and counterproductive.

Hence I wanted here to list some of the things that I took to be for granted for the design to have. That is, if the proposal does not preserve any of these properties then it should be deemed a failure:

• Intent-support
• Compositionality
• Privacy

I will not elaborate on exactly the details of these terms, but hopefully for those who have worked with the resource machine these will make sense. In practical sense we want to support solving and support shielded-state transitions.

Finally, in terms of who gets to decide whether there properties are preserved, it would be the cryptography team, namely @vveiln and @xuyang. If the cryptography team - the core designer of the current architecture - is not convinced of an alternative design then this is a very clear sign that something isn’t working. In this sense I think it makes sense to make the final instance of any ideation on this topic to be the cryptography team.

Given all that, we can come to the ideation itself:

---

1. pun unintended ↩︎

[ArtemG]

Ideation

The approach was simple and I thank @graphomath and @mariari for being able to listen to my ramblings regarding it.

The approach was basically: look at QTT and try to map the concepts that it has to the already-existing RM concepts. If these concepts already exists: great, try to interpret them literally. If not, think of ways of incorporating these.

All the images used in this post can be accessible from an excalidraw here.

The Model

There are of course proper methods for defining what a model of a TT is, here I will be mostly handwaving hoping that it will get people interested in this direction.

Core TT

So what do we need to model in order to make sense of what a type theory is? Well, the central notion of a type theory is a judgement. There are practically two sorts of judgements: whether a type is well-formed in a certain context or whether a term of a certain type is well-formed in a certain context.

This makes it clear that what we need to define is:

1. what does it mean to be a type in RM
2. what does it mean to be a term in RM
3. how to make judgements in RM

Let us assume we are in a non-dependently typed environment. Then more-or-less what you need in order to formulate what a type is is its

1. introduction rules
2. elimination rules
3. syntactical name

Introduction rules allow you to say when that type can be introduced (by introducing its term), elimination when a term of said type can be used. A name is just that: a name. Similarly how we can name booleans Bool or bool or bOoL.

This I would say maps fairly easily to the concepts of

1. Resource logic when we create a resource
2. Resource logic when we consume a resource
3. The resource label

I don’t think this particular connection is controversial for us, we have worked with it for quite a while.

And of course this all seems to correspond indeed to a notion of an RM kind:

Now we come to a notion of a term. A term fundamentally has three constituents:

1. a type
2. a syntactical name
3. dependencies

We already know that what we want is to have a correspondence between a term of a type and a resource of a specific kind. We know that kind corresponds to the type, we can associate value with being a syntactical name, although that is not quite how we use it currently.

The hardest thing for us to map here is I think a notion of “dependency”. This is something that has been giving us headaches during the controller development process. We do not have a formal notion of dependencies. It is currently split through being something application-dependent (something that a resource logic asks for explicitly) and application-independent (balancing resources seem to be something that commonsensically is a dependency yet is not seen in resource logics).

So here, I propose we actually introduce a separate field called “dependencies”. As dependencies are multiple and term dependencies are on other terms, it seems natural that dependencies of a resource are some sort of an array of resources (or references to them, we’ll come to that at some point)^[1].

All-in-all, at this point we have deduced that we need something equivalent to three fields in the datatype:

That is not the end of it, however, as we go further into the needs of the system, we will need to adapt further.

The first thing to note is that we agree to these descriptions we sort of agree to the fact that a RM transaction corresponds to some derivation, sequents such as e.g.

In this sense the entire history of Anoma executors/controllers (those that run RM algorithms to check state changes and enforce them) can be seen as just an ever expanding derivation tree:

Global IDs/Commitments/Nullifiers

Here we come to identification of resources. What is different between two statements that say true : Bool, i.e. generate a boolean. Generally nothing, on the “underlying TT” level they are just the same term syntactically. However they are different in computation and use. Here we come to the reason why people bear with De Bruijn indices: we need a way of identifying terms which are syntactically the same but practically different. Moreover, we need to do so “globally” across several derivations/transactions. Even more moreover, we need the identification to be somehow “hidden” so that creating and consuming the resource can be made hard to link.

That is, we need a way of incorporating the ZCash commitment/nullifier architecture. Here is where we need the resource to have two more fields: nonce and nullifier key (commitment).

These grant that globally two “syntactically same terms” (read as: resources with same kind, value, and dependency fields) are seen as different. The nullifier key is of course needed for nullifier creation.

Note that from this perspective there is a notion of a term and of additional identification/privacy information. Practically a distinction between something like a “core resource” and “core resource with identitifcation/privacy info.” This idea of a “core resource” has been something that I have heard quite a wile ago from e.g. @jonathan, it’s not a new concept in research folks trying to grasp the RM.

But for the time being, let us bar specific naming and focus on the function. So now we have expanded the resource datatype to contain:

with the idea that nonce is used to derive the unique ID (commitment/nullifier) connected to the term and nullifierKey to conceal usage information (decouple commitment from nullifier).

QTT

Finally, we come to the actual QTT part, namely introducing the concept of quantity.

Here, I am unsure what would be the best way of introducing this or specifically what kind of QTT we want. We may want to either do the usual QTT over the “natural linear-affine” semiring as I described before or “unite” two QTTs: affine and linear. More on this distinction may be read about here.

However here let us bar this particular discussion. My personal opinion is whatever we introduce below may stand in correspondence to either one of the two approach above.

First things first, we need to now introduce an extra concept to the notion of a resource, quantity:

Note that quantity here will properly speaking be interpreted as quantity of a resource, not of a type. This is an important distinction with the current state of things and the hardest part to reconcile with current application designs.

The difference can be spotted in semantics. Currently when we consume 500 quantities of a resource we usually think of it as “I consume 500 of that resource.” In this mode we think of it as “I consume a resource 500 times.”

Note that, however, in this model for us quantity is not just a number but an element of out “natural linear affine” semiring mentioned in the Ideation Setup.

To make things more explicit, let us present it in a way that is similar to the current implementation:

where isEphemeral can be seen as isLinear flag. That is isEphemeral = true means that it is a linear quantity where isEphemeral = false affine.

The idea is hence that in a single transaction - a single derivation step in the sequent tree - linear resources need to be used exactly the number of times declared in said transaction. They are introduced in the runtime of a transaction and consumed in the same runtime. Think intents: you introduce them to be solved in the span of one derivation.

Affine resources - on the other hand - are those that you want to possibly span several derivations. These are persistent resources. These are the resources you may want to create in one derivation but consume way later, such as a proper token.

This has implications for the delta. The computations becomes nuanced:

Definition of “resource being consumed” is not per-se defined by the transaction having nullifiers but by it being dependency of some other resource. Moreover, we now practically would need to have two deltas: one for linear and one for affine resources.

This is probably the hardest thing to reconcile both with the current cryptography tech we use and with application development. The process I describe in computing delta is fairly convoluted and will require proper thought to be made sure it cannot be abused. Moreover, it requires us understanding when deltas have a “positive balance.”

So the idea is that only resources created actually “influence” the delta. In type theory the definition of being “consumed” can roughly stand to being passed as a variable to a generation of another term, i.e. be a term dependency.

So given a transaction T such that linear resources R1_Lin,...,Rn_Lin and affine resources R1_Aff,.., Rk_Aff are created, we calculate the delta by summing the quantities of said created resources and subtracting quantities of the resources listed in their dependencies multiplied by all resource fileds other than the nonce field. With linear and affine deltas computed differently.

As an example, consider two resources:

If they are in the same action, then the delta will be computed:

For linear resources as:

1 * hash(R1.kind, R1.value, R1.nfKey)

For affine as:

– 2 * hash(R2.kind, R2.value, R2.nfKey)

The evident question of “how do we ensure that resource logics of the things listed in dependencies pass,” this can be resolved by passing the action tree root to the compliance units and ensuring that all the dependencies are consumed inside the action.

Note, however, that even if we consume R2 to be part of R1 dependency, we may want to use it only 1 time. So the dependency list needs to contain how many times we use the resource as well. So the dependencies become something like a list [(resource, usedQuantity)] akin to:

with the delta being computed appropriately, subtracting only one instead of two.

In terms of what which transactions we then deem to be able to influence state change:

It is those transactions which produce a balanced linear delta and positive affine delta.

This I think is enough abstract ideation. Here we can move towards concrete implementation details:

---

1. Note that here I will talk about plaintexts of dependencies, not necessarity how they will be represented in the final datatype, similarly how we can talk about a resource having a logic but what a datatype has is a logicRef ↩︎

[ArtemG]

Ideation on Concrete Changes

Here we try to formalize the changes proposed above in abstract as concrete proposals about changing the datatypes and proof circuit descriptions of the current RM design. Note that - given that the ideation above is somehow suitable to be used - that the concrete implementation details I propose below are sound. Possibly some of them are plain incorrect and some poorly done. Certainly not all of them I have knowledge of how to actually implement.

Resource

The resource datatype now has a field dependencyRef. It is fixed-size. Its plaintext is intended to be a list of tuples (nullifier, quantity).

Compliance

Compliance Instance

Compliance instance now contains actionTreeRoot.

Compliance instance now contains LinearUnitDelta and AffineUnitDelta instead of the usual unit delta.

Compliance Witness

Now contains not only the resource plaintexts but also an explicit plaintext of dependencyRef which is a list of fixed-size hash pairs, which represent the nullifiers of the resources used in the dependency alongside their quantities used in said particular resource creation. Alongside that, the plaintext of each of said hashes with the nullifier keys to ensure that the nullifiers match.

For each of such nullifiers, we expect a path to it at the action tree root.

Add LinearRCV, AffineRCV instead of one RCV

Compliance Proof

As mentioned, alongside the usual checks, check all dependency lists are derived correctly, check all nullifiers of dependencies exist at the action tree root using provided paths.

Reject all resources used with quantity 0 in dependencies.

Check the deltas for linear and affine resources separately by computing them. Recall that delta of a resource of bool ephemerality created corresponds to adding R.quantity * hash(R.kind, R.valueRef, R.dependencyRef, R.nkCm) to the appropriate delta part (linear if bool = true) and if a resource is used in the dependency, subtract quantityInDependency * hash(R.kind, R.valueRef, R.dependencyRef, R.nkCM)

Delta

Here I profess my ignorance: I do not know how to exactly implement the checks I describe here for the affine case. I do know that we were researching possibly using positive deltas, which is why I was thinking this may be possible. However, I may be completely wrong.

Delta proof would be now two-part. One part for checking the linearity delta, which should be balanced. The affine delta can be unbalanced, as long as it is positive.

[ArtemG]

Conclusions

Based on a tight timeline, I cannot say that I was able to properly give this research project a spin it required. At the very least I was planning on trying to adapt AnomaPay to the current design decisions to personally ensure that it works and all properties are preserved.

Lacking this, I do not have too much conviction that this approach will work.

Alongside that, while the model of the RM gets simplified by the changed proposed, the implementation certainly doesn’t. It seems we need to complicate the compliance circuit more, alongside introducing the tricky delta computation.

However, there are still two positive spins on this ideation:

1. We finally have a proper notion of dependency
2. We finally have a good compilation target

That is, this approach - I am fairly certain - can help with the Dagon stack. However, maybe not exactly this approach. Possibly there is some other type theory that can be proposed, maybe we can find a type theory much closer tied to the already-existing RM design.

Even then, even if we accept that the model is what we want, the RM is hard to make sense of other things. What do witness data not represented by resources stand for? What about payloads?

All-in-all, as it stands right now, I consider the result of this ideation to be a failure as I have not properly given a model that I think would be convincing. I think, however, that the approaches and some insights here may be used to expand this into a successful ideation. Hopefully it will.

[graphomath]

@ArtemG

Privacy

Footnote:

A very similar type system can be used to reason about information flow.

[isheff]

From a meeting at 2025 December HH:

It looks like we can implement what I called “empty actions” with actions involving ephemeral resources and intent resources. This makes them not “empty,” but doesn’t require changing much that’s interesting. The “>” proof would then be part of the resource logic of… the intent resources?