Proposal: Towards QTT Semantics of RM

[ArtemG]

Preamble

As a result of Jeremy’s model I reread some papers on QTT and was thinking how we may want to change the current RM model to allow more rigid cross-action checking as well as making it closer to proper Quantitative Type Theory.

A question that I was posing myself is: what is the quantity field really about if not for usual quantity as in “I want X quantity of XAN or spacebucks”. The answer is, of course, that it is supposed to be quantity in the sense of quantitative type theory: “I want this specific resource to be usable X many times”.

In other words, this is a field that controls linearity, i.e. how many times can we use a resource (in the logical sense of resource). There are, moreover, two levels of linearity: global and local for the RM. Global linearity’s goal is to check that no resource can be consumed which has not been created and check double spending and creating. This is handled by the commitment/nullifier RSM mechanism. Now, the local linearity constraint is handled by the Delta Proving System. It says that we need to balance the kind of resources created an consumed. Ideally, the QTT semantics tells us that actually it is not the “kind” of a resource that we want to control consuming but resource itself (more on that later).

Alongside this observation, I started asking myself what does ephemerality really do on the RM level. It has only one functional difference: it does not require global linearity check (it can be consumed without previously being created); and one practical application (modulo logic triggers which is not important in this context): it can balance local linearity check (deltas). PS: Maybe also for balancing Compliance Units for cases where Compliance Instances need to be balanced in terms of created and consumed resources.

This brought me to another question: do we ever really care that a non-ephemeral resource has some local linearity using semantics described by, again, Jeremy’s post? The answer to me seemed to be “no”. We only care about local linearity if we have some intent-bearing resource onboard. Usual things like “spacebucks”, “XAN” etc which use other parties do not assume that we create and consume things in the same action. (here I might be wrong, please let me know if I am)

In other words, things that we care locally (i.e. in terms of local linearity) are exactly things which trigger intents logics. They are there to be created and consumed, which would correspond to them being fulfilled. They can also be created an consumed several times in case you want that constraint to be fulfilled several times. All of this can be encoded as a non-zero value of the quantity field.

This brought me to the following proposal:

Proposal

1. Remove ephemerality field from a resource (their role will be played by non-zero quantity resources)
2. Compliance Proof check skips root check in case the resource they are using has non-zero quantity.
3. Delta’s preimage does not have resource kind as keys. Instead, it has the hash of a larger part of a resource, including logic, label, value, etc. I would say “everything but quantity” should be the key.

This corresponds to Jeremy’s requirement of requiring intent-bearing resources to be consumed in the same transaction (delta check ensures this), simplifies the design, and makes the RM closer to QTT.

Specifically:

Consequences

• Usual resources we care about globally (like XAN, spacebucks, whatever) have 0-quantity. Their linearity is checked during global checks.

• Intent-bearing resources exactly correspond to non-zero quantity resources. The new delta check ensures that the full resource is both created and used (sans quantity and other minor data we might want to skip).

• Deltas actually track resources (or at least something closer to our definition of a resource, i.e. covers more data) and not kinds of resources.

• Might be a bit cumbersome to make sure we have enough resources for compliance proofs for shielded case as they might require e.g. exactly one created and one nullified in the instance, but nothing I see as essentially problematic, just a bit inconvenient.

PS

If I am not mistaken Jeremy’s issue can also be fixed using only the last part 3 of my proposal. Namely make deltas account for the entire resource sans quantity. The ephemerality removal jumps at me though as the next logical step due to the prior discussion.

[graphomath]

@ArtemG

Quantitative Type Theory

The syntax and semantics of quantitative type theory - Strathprints

[ArtemG]

Just in case: I am not claiming any formal correspondence here. Just trying to stay closer to the proposed informal intuition of quantity ~ usage accounting.

[xuyang]

It appears you redefined quantity and delta proof? What about linearity checks in your context? I’m not sure I fully understand it.

In the current design, we highly recommend using the quantity and delta proof by default for balance verification since relying on application logic to check the balance can be risky. However, this is not mandatory. I notice you want to put the amount to the value and check the balance in the logic. To skip the RM-provided balance check, you can set resource quantities to zero in your app and encode amounts into values if confident in your app logic. Note that this may complicate balance checks, requiring extra ephemeral resources or logic since the logic only accesses resources in the current action. I believe you’ve noticed that in Jeremy’s examples. Additionally, delta and linearity checks might not help with your balance verification and cannot interpret your value format which is defined by your application.

@ArtemG

Delta’s preimage does not have resource kind as keys. Instead, it has the hash of a larger part of a resource, including logic, label, value, etc. I would say “everything but quantity” should be the key.

I’m confused about the proposal 3. If we don’t use kind as keys, the nonce or random_seed must differ for each resource. Additionally, your XAN tokens and my XAN tokens will have different delta preimages because our public keys in the value are distinct. What checks are you performing on delta?

[ArtemG]

Thank you so much for your response!

It appears you redefined quantity and delta proof ?

Indeed, I want quantity to correspond to the quantity in the sense of Quantitative Type Theory: how much can a specific resource can be used in a specific derivation (transaction). In this sense delta does not track the kind of resources but resource datatype sans quantity as you mention later in the post. I will try to elaborate on that below.

I notice you want to put the amount to the value and check the balance in the logic.

Right, here I should have made clear what my presuppositions are. Specifically, I assume as a given in my proposal that we want to pursue @mariari’s model as detailed here. That indeed hides the amount of a specific resource for which the concept “amount” can be specified in the value.

Note that this may complicate balance checks, requiring extra ephemeral resources or logic since the logic only accesses resources in the current action. I believe you’ve noticed that in Jeremy’s examples.

Right, as mentioned, I follow Jeremy’s example. Here let us assume my original proposed model (proposals 1-3). I can try to explain how I see this happening on a high level by basically paraphrasing Jeremy’s example of spacebucks in a transparent resource machine. I will even simplify it further for the sake of the argument.

First define a resource kind FixedSupplyIntent by defining its logic. Its logic is as follows:

If I am created, return true. If I am consumed, then look into my value field (as we are doing things transparently I assume the value is just a list of 3 elements: [quantity, kind, should-create?] I do have to be honest I am unsure what happens here in shielded case). I then check that

• If should-create?=true that there is a resource R of kind kind has been created in the action such that R.value = quantity
• If should-create?=false that there is a resource R of kind kind has been consumed in the action such that R.value
  and return the appropriate boolean

Now we can define a Spacebuck kind by defining its logic. Its logic is as follows:

I look into the tag provided in the instance with the flag checking whether I am a RL of a created or consumed resource. Based on this, I search the preimage of my tag by either committing or nullifying the resources provided in the action. If I find the appropriate resource R then I compute its kind, name it kind.
Then I look through all resources in the action and make sure that I can find a FixedSupplyIntent resource R2 such that R2.value has the same kind in it as kind and same value as my value with appropriate should-create? value. I return true iff all the check above succeed.

With this, I we are ready to describe what “ammount control” for a resource can be without using quantity following my example.

Here, define R_space to be the spacebuck resource with R_space.value = 5, R_space.quantity = 0. So suppose I want to consume R_space and I want to create the same amount of spacebucks. I then define R_space2, a Spacebuck with possibly some other nonce, random stuff, but same kind and same value of 5.

Then I need one more resource: R_intent which is of kind FixedSupplyIntent. R_intent.value = (5, Spacebuck_kind, true) and R_intent.quantity = 1.

So overall, we have three resources: R_space, which I want to consumed, R_space2 which I want to create and R_intent which will take care that I create exactly as much as I consume.

We form two actions for the transaction:

• Action 1
  • Consumed: R_space
  • Created: R_intent
• Action 2
  • Consumed: R_intent
  • Created: R_space2

Based on my proposal, the delta check will be: check only intent resources, i.e. non-zero quantity resources. Moreover, check that the delta proof is not over kinds but over the entire resource sans quantity. Using such a definition a Tx with only two of the above actions will balance. However, if we changed anything about the value field of R_intent, this check would fail.

Here I have showcased how to use my approach with Jeremy’s example, putting all relevant data into value with delta-check not allowing to tamper with the value field of the intent.

Additionally, delta and linearity checks might not help with your balance verification

I would say that the above demonstrates how it might help with balance verification, doesn’t it?

…cannot interpret your value format which is defined by your application.

So here I can say that I seem to have provided an example for the transparent case where given a trivial app structure (fixed supply app) we know how to inspect the value field. The app determines how the value field is structured which also allows the logic to check specific fields. The app above determines both Spacebuck and FixedIntentResource value field format for example, at least that’s how it appeared to me (correct me if I am wrong @mariari)

In shielded case, though, I profess my ignorance. Here you know better whether it will work that way.

If we don’t use kind as keys, the nonce or random_seed must differ for each resource

I am unsure whether this is important in our case, but I might be ok with skipping the nonce and random_seed fields for as part of the delta preimage keys as I do not see when that information may be intent-relevant.

Additionally, your XAN tokens and my XAN tokens will have different delta preimages because our public keys in the value are distinct.

That is fine, since XAN is an actual proper resource, not intent-bearing resource. We care about XAN beyond it getting spent in the same TX as it was introduced, so XAN should have via my approach quantity 0, i.e. it is basically ignored by the delta proof. XAN should always balance, i.e. if you use it you should always make its quantity 0. This is similar to how in variants of linear logic with non-linear types you mark which ones are and are not to be used linearly. What will check its ammount balancing are the resource logics as described above for Spacebucks.

Hope this made it a bit clearer!

[cwgoes]

@ArtemG

Indeed, I want quantity to correspond to the quantity in the sense of Quantitative Type Theory: how much can a specific resource can be used in a specific derivation (transaction). In this sense delta does not track the kind of resources but resource datatype sans quantity as you mention later in the post. I will try to elaborate on that below.

The current formulation is intended to capture something a bit different: namely, resources of the same kind (in the RM sense) are of the same type (in the QTT sense), even if they have different values (in the RM sense). One might understand the set of possible resource values for a particular resource kind as the set of members of a sum type defined by the kind (which commits to the logic that ultimately defines the set of values with which resources could actually be created).

While your proposal – as I understand it – should be of equivalent expressive power in terms of application construction (as compared to the current ruleset), it would have us forfeit the ability to make this type/instance distinction in the “resource linear logic”. This means that we would need to build the linear logic for the type level on top, e.g. have rules for summing up the value fields of various Spacebucks resources and checking that the sum of the value fields for consumed Spacebucks is equal to the sum of the value fields for created Spacebucks. This is possible, but it seems inelegant to me – we already have a programmable linear logic, why not use it? – and will create additional complexity in the shielded case (we would have to implement another layer of homomorphic value encryption).

n.b. I can understand that ephemeral resources are awkward to use for some constraint-passing purposes at the moment, but I think we can fix that problem in a different way, which I outlined here. Even if we don’t take that approach, I don’t think we need to go so far as to ditch precise control of the linear logic in order to fix the developer ergonomics.

Does this help clarify the design intention? I admit that the connection to QTT is little more than “we read the QTT paper, read the Zcash specs, and figured out how to mesh them together in some way that seemed reasonable, gave us a type/instance distinction, and preserved the nice homomorphic commitments from Zcash” – we haven’t ever formalized what this “resource linear logic” is really supposed to be at a slightly higher level of abstraction, and I think the project of doing so may prove quite rewarding.

[ArtemG]

Thank you for the response!

As I see it, your comment touches two main points:

1. The proposal will require extra complexities for the shielded case.
2. It is inelegant as we lose programmable linear logic.

I want to argue against both of these points.

Shielded Case Homomorphism Property for Delta Hash

You mention that:

we would have to implement another layer of homomorphic value encryption)

Could you elaborate why you think that? Here, I am referring to the spec of the delta hash which seems to claim not the homomorphic property over specifically kinds but over the codomain of the kind hash. You can also see this in my formalization and from my understanding what also happens in the e.g. Pedersen Commitment Scheme. Now, I am not proposing somehow introducing an extra argument to the delta hash. I am proposing to introduce a general hash r_hash valued in the same field the kind hash is currently valued over. As long as we can implement that (which I think should be trivial but here I will check in with relevant parties) we do not need any additional homomorphic properties. We can use the same delta hash, e.g. Pedersen commitment scheme.

Does this clear up my proposal?

Linearity

Here, as we do not have any formal correspondence as you mentioned before, we have to engage in a bit of scholasticism. But I will try to make my position a bit clearer by using some informal correspondences.

Here are my assumptions:

• Resource kind corresponds to a type
• A resource instantiation corresponds to a term of a type
• Resource quantity corresponds to the semiring value for usage accounting.
• A commitment to a resource of quantity n corresponds to the judgement that the appropriate term is of appropriate type and the term has n value of the semiring attached for usage accounting (i.e. term/variable declaration)
• A nullifier of a resource of quantity n corresponds to the judement that the apporpriate term has been used the appropriate n quantity of times.
• Delta proof balance corresponds to checking that if a term has been declared to be used n times that is exactly how much it was used at runtime
• Transaction corresponds to runtime

Here, we come to your comment:

it would have us forfeit the ability to make this type/instance distinction in the “resource linear logic”

I do not see why this would be the case. A type-instance distinction is kept. Nobody is forbidding you to compute the kind of the resource. Indeed, in the example of my original post, we do use this type information as that is what we keep in the FixedSupplyIntent. Its resource logic indeed checks that we have a specific type of resource (i.e Spacebucks) created first before anything else.

we already have a programmable linear logic

Here is where I would like to disagree with you due to a specific issue with deltas. As you mention and if you accept my correspondences laid out above, quantity of a resource corresponds to the particular semiring value for usage accounting.

Now, consider this: what does the delta proof check? The delta proof currently checks that the kinds of resources used are balanced. Now ask yourself this, is this what is being done on the type-theoretic level?

Let us return to my axioms:

" Delta proof balance corresponds to checking that if a term has been declared to be used n times that is exactly how much it was used at runtime"

Note, that quantity is not a property of a type, it is the property of a term belonging to a type. You can see this in the original paper on page 4 where they declare a Boolean type (no accounting info needed for that) but then define the terms as having computational info. (This is also how it is in the RM design currently: quantity is something belonging to a resource not of a kind of resource)

You can also see in the Idris implementation paper where in the context of the zero-one-many semiring they explicate the meaning of these values as:

0: the variable is not used at run time
1: the variable is used exactly once at run time
ω: no restrictions on the variable’s usage at run time

The quantity is of a variable not of a type.

Now, suppose we have some resource kind K. In type theory this would correspond to having some type K. Now suppose we have a transaction with resources R1 and R2 of kind K both of quantity 1. Suppose R1 is consumed and R2 is created. Now, this passes delta check. But it is actually impossible to derive this in type theory land using the correspondences laid out. Why? Because you just spent the resource R2 which was never declared! In our context we only have

R_1 :^1 K

we cannot spend R2 because it was never announced to have existed, it is not in the context to be used.

As a second case, suppose we have the same scenario but we create both R1 and R2 and consume R2 twice. (this will of course not pass the uniqueness check but here I am arguing specifically regarding the delta proofs) This will also pass the delta check as the kinds balance. However, in the QTT land, this also is not derivable. Why? Because you declare R2 to be able to be used once and not many times. You do that by declaring its quantity to be 1.

In other words, what the delta currently keeps track of is the quantitative information of the type. But that is wrong on the QTT level as quantity is not information of the type but of the term in the type system.

Having

true :^1 Bool, false :^1 Bool

does not mean you want to balance the use of any terms of Bool at runtime to be 1 + 1. No, what you want is to check that true is used exactly once and false is used exactly once.

Which is exactly what my proposal is trying to achieve.

we haven’t ever formalized what this “resource linear logic” is really supposed to be at a slightly higher level of abstraction, and I think the project of doing so may prove quite rewarding.

I agree Exactly why I am trying here to draw as many concrete parallels as possible

Hope this clarified my stance! Let me know what you think!

[cwgoes]

Thanks for the detailed exposition! I think we’re making progress here.

@ArtemG

As I see it, your comment touches two main points:

1. The proposal will require extra complexities for the shielded case.
2. It is inelegant as we lose programmable linear logic.

Yes, that’s an accurate summary of my concerns. I’ll split my response into two sections accordingly.

---

(response re: concern 1)

@ArtemG

Could you elaborate why you think that? Here, I am referring to the spec of the delta hash which seems to claim not the homomorphic property over specifically kinds but over the codomain of the kind hash. You can also see this in my formalization and from my understanding what also happens in the e.g. Pedersen Commitment Scheme. Now, I am not proposing somehow introducing an extra argument to the delta hash. I am proposing to introduce a general hash r_hash valued in the same field the kind hash is currently valued over. As long as we can implement that (which I think should be trivial but here I will check in with relevant parties) we do not need any additional homomorphic properties. We can use the same delta hash, e.g. Pedersen commitment scheme.

Yes, this seems plausible enough (although I’d defer to @xuyang on the details) – this isn’t my concern, my concern is that applications would need to separately implement a linearity check in order to achieve the behavior that they can currently leverage the balance check to get, and that this separate linearity check would also need to use a homomorphic commitment scheme if the developer wants to “manually” perform linear checks with the same privacy properties that they can currently use the delta to perform.

Two examples, one simple, one more complicated:

1. Let’s suppose that I want to split my 5 Spacebucks into one resource of 2 Spacebucks and one resource of 3 Spacebucks. As you have defined the Spacebuck and FixedSupplyIntent logics, I do not think that would be possible, we would need to modify at least one of them (e.g. the FixedSupplyIntent logic) to instead scan all the Spacebuck resources within an action and sum up their values (e.g. we would need to reimplement the linearity check).
2. Let’s suppose I want to swap 5 Spacebucks for 5 Typebucks (intent A), you want to swap 2 Typebucks for 2 Spacebucks (intent B), and Jeremy wants to swap 3 Typebucks for 3 Spacebucks (intent C). In the current (“kind-delta”) RM, a solver S can compose intents A and B into A \circ B and send it to another solver S', where S' need not be told the original amounts of 5 and 2, but only the remaining amount of 3, in order for S' to match A \circ B with C, resulting in a balanced transaction. How would similar privacy properties be achieved with your proposal? I suppose that you could alter the FixedSupplyIntent resource logic to admit a “partial satisfaction” of the constraint where you can e.g. consume a FixedSupplyIntent(5 Spacebucks) resource to create a FixedSupplyIntent(3 Spacebucks resource) + a 2 Spacebucks resource, effectively carrying forward part of the constraint to be satisfied later. Is that what you would envision? This seems workable in principle, but it would introduce a cost (in terms of number of constraint-carrying resources) proportional to the number of times which you utilize the linearity relation in a particular transaction, which seems potentially problematic from an efficiency perspective. Maybe you have a better design in mind?

---

(response re: concern 2)

@ArtemG

• Resource kind corresponds to a type
• A resource instantiation corresponds to a term of a type
• A commitment to a resource of quantity n corresponds to the judgement that the appropriate term is of appropriate type and the term has n value of the semiring attached for usage accounting (i.e. term/variable declaration)
• A nullifier of a resource of quantity n corresponds to the judement that the apporpriate term has been used the appropriate n quantity of times.

Those are also working assumptions of mine.

@ArtemG

• Resource quantity corresponds to the semiring value for usage accounting.

This too, but do note: in our case we can actually assume a ring structure, i.e. we have additive inverses (negative quantities), and in fact heavily rely on them.

@ArtemG

• Delta proof balance corresponds to checking that if a term has been declared to be used n times that is exactly how much it was used at runtime
• Transaction corresponds to runtime

Here I am not sure that we have the same correspondence in mind. I had rather seen the transaction as a derivation in QTT, where the delta proof balance corresponds to checking that the derivation “balances out”, e.g. in the end, the sum of the quantities of all resources of kind K (terms of type T) created is exactly equal to the sum of the quantities of all resources of kind K (terms of type T) consumed. This is somewhat different than QTT in a few ways:

• We have additive inverses for usage annotations (a full ring). This actually violates a condition in the paper which requires that the semiring be positive.
• We have an introduction rule allowing us to introduce both a resource of kind K and quantity Q and a resource of kind K and quantity -Q (I guess this replaces the “Ext” rule in the QTT paper) into the context.
• We have an elimination rule allowing us to take a resource of kind K and quantity Q and a resource of kind K and quantity -Q and remove both of them from the context.
• Instead of checking the correspondence between some declaration and actual usage in runtime, we’re checking that the derivation itself is valid.

In this sense, the correspondence I had in mind is more like classical linear logic but with a ring of quantities instead of just 0 / infinite which is more typical in the literature.

@ArtemG

I do not see why this would be the case. A type-instance distinction is kept. Nobody is forbidding you to compute the kind of the resource. Indeed, in the example of my original post, we do use this type information as that is what we keep in the FixedSupplyIntent. Its resource logic indeed checks that we have a specific type of resource (i.e Spacebucks) created first before anything else.

The distinction is kept, yes, but the linearity check is unaware of it – in your proposal, the linearity check would act on the whole resource level, not just the type level. I think you are right that this is closer to McBride’s QTT construction, which does not allow the kind of “type-quantity-level” introduction or elimination which I describe above, but I do think that we are reducing expressivity here, in the sense that developers can no longer choose which parts of their resources are supposed to count as part of the type (which is linearity-checked) and which are not.

@ArtemG

You can also see in the Idris implementation paper where in the context of the zero-one-many semiring they explicate the meaning of these values as:

0: the variable is not used at run time
1: the variable is used exactly once at run time
ω: no restrictions on the variable’s usage at run time

The quantity is of a variable not of a type.

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.

@ArtemG

Now, suppose we have some resource kind K. In type theory this would correspond to having some type K. Now suppose we have a transaction with resources R1 and R2 of kind K both of quantity 1. Suppose R1 is consumed and R2 is created. Now, this passes delta check. But it is actually impossible to derive this in type theory land using the correspondences laid out. Why? Because you just spent the resource R2 which was never declared! In our context we only have

R_1 :^1 K

I’m not quite following this example – you say that R2 is created, but then that you just spent the resource R2 which was never declared? I assume that by “spent” you mean consumed. Are we also consuming R2 (in which case this transaction wouldn’t be balanced)? Even if that was just a typo, aren’t we declaring R2 when we create it? If not, when do we declare resources, in your system?

@ArtemG

In other words, what the delta currently keeps track of is the quantitative information of the type. But that is wrong on the QTT level as quantity is not information of the type but of the term in the type system.

I agree that the current RM implements a quantity-sensitive linear logic (better not call it QTT) which is different from QTT in this way, yes. I’m not yet convinced that the system closer to QTT which you propose is better than the one we have, though – in fact, I think if you really want this system, it should be possible to instantiate it simply by putting all data in the label (instead of the value) – would that work? If it would, then is that sufficient for your purposes, or if not, why not?

In any case, I’m fully in support of explicitly specifying this quantity-resource-linear-logic, whatever exactly it is.

[ArtemG]

Thanks again for responding!

Two examples, one simple, one more complicated:

I agree that these are nontrivial. I actually posed the same problem to @mariari himself the first time he showcased the fixed-supply-mixin. Here I would say - as I mentioned in a response to Xuyang - that I accept @mariari’s model as an axiom and hence I accept that amount of resources are stored in the value field. Here he promised me that this case can be handled well and I trust him that it can, so here I will call upon his help. @mariari I think this is fine, right?

Do note that the examples you bring up as possibly problematic are touching upon essential topics of @mariari’s proposal, not specifically mine as it is not central for my proposal to store amount information in value and make resource logic checks anything related to it, it just builds upon it.

and that this separate linearity check would also need to use a homomorphic commitment scheme if the developer wants to “manually” perform linear checks with the same privacy properties that they can currently use the delta to perform.

What would I need homomorphism over? Is there a computational purpose here? I described the resource logic for the application above and did not seem to need any homomorphism, so I am unsure what exactly should be done here, but maybe this is just me being ignorant of the cryptography.

This too, but do note: in our case we can actually assume a ring structure, i.e. we have additive inverses (negative quantities), and in fact heavily rely on them.

Ok, right, but here we do need to be specific in saying that 0 in QTT land and 0 in RM land is different. 0 in QTT land means that a variable in not used at all in a derivation. For us it means something else, more like: it is unchecked, closer to “many” element of the ring. Which also makes sense since the usual resources like XAN are checked for global linearity first and foremostly.

I had rather seen the transaction as a derivation in QTT

This is I think exactly what is meant by “runtime” in the Idris paper.

where the delta proof balance corresponds to checking that the derivation “balances out”, e.g. in the end, the sum of the quantities of all resources of kind K (terms of type T) created is exactly equal to the sum of the quantities of all resources of kind K (terms of type T) consumed.

As discussed, this is not something that QTT does or is aimed to do, types themselves do not possess quantity-assurance information, but I see below you already see how this model differs from QTT.

This is somewhat different than QTT in a few ways

Right, so if your point is not to model QTT then I am fine with that. My argument came from assuming that we were aiming for a QTT-like system and weren’t modelling it properly. If it is not our goal to model it, this is fine.

The other side of the coin is for @mariari to decide if this actually solves his issue which he posed originally and for which this proposal is also tailored. I will address this below.

I assume that by “spent” you mean consumed.

Oh I am so sorry, that is indeed a typo. I meant to say that “I just spent the resource R1 which was never declared!”

Here I assumed formally that R1 is an ephemeral resource (and hence I can create it without it having been created before).

Even if that was just a typo, aren’t we declaring R2 when we create it?

Due to my original correspondence with which you agreed variable declaration ~ commitment. So if we just consume R1 we never declared it in TT land. So yeah, it was about R1, hope it clarifies this, sorry!

if you really want this system, it should be possible to instantiate it simply by putting all data in the label (instead of the value) – would that work? If it would, then is that sufficient for your purposes, or if not, why not?

Here the reason is @mariari’s system. This proposal was build around allowing his approach to work. In his approach, he moved away from quantity as storing amounts of resources, and he mentioned parallels to QTT so I tried to both 1) solve his problem 2) make sense of quantity field using type theory.

In other words, as @mariari does not want to put things into the label, neither do I in this specific proposal.

PS: But this approach (of putting everything into label) does indeed seem equivalent to the proposal with our current setup. Although we do lose the type-term distinction, we can now only differentiate via logic.

Just to wrap up, all in all: my argument had two sides.

1. My proposal is closer to QTT
2. My argument solves the problem @mariari faces with storing app-relevant info in the value field

1 only makes sense if we indeed are pursuing QTT semantics. You mention that that is not a goal in and of itself and that the delta check indeed is not related to QTT right now. So I will drop that line of defense as it seems irrelevant whether we are close to QTT or not.

[cwgoes]

@ArtemG

Do note that the examples you bring up as possibly problematic are touching upon essential topics of @mariari’s proposal, not specifically mine as it is not central for my proposal to store amount information in value and make resource logic checks anything related to it, it just builds upon it.

It is true that amount information would not necessarily need to be stored in value with this proposal, it could be stored elsewhere, but if it affects fungibility (i.e. included in the delta preimage in the linearity check), then a developer must implement a separate linearity check as I have described – and my understanding of this proposal is that everything in a resource affects fungibility, so that would entail this requirement.

@ArtemG

What would I need homomorphism over? Is there a computational purpose here? I described the resource logic for the application above and did not seem to need any homomorphism, so I am unsure what exactly should be done here, but maybe this is just me being ignorant of the cryptography.

Homomorphic commitment addition simply allows a third party to add (or subtract) commitments without knowing their preimages, such that only a + b would be a valid opening of commit(a) + commit(b). This can be used for privacy in compositional solving, such as in the example I described.

@ArtemG

Ok, right, but here we do need to be specific in saying that 0 in QTT land and 0 in RM land is different. 0 in QTT land means that a variable in not used at all in a derivation. For us it means something else, more like: it is unchecked, closer to “many” element of the ring. Which also makes sense since the usual resources like XAN are checked for global linearity first and foremostly.

Yes, good point.

@ArtemG

Due to my original correspondence with which you agreed variable declaration ~ commitment. So if we just consume R1 we never declared it in TT land. So yeah, it was about R1, hope it clarifies this, sorry!

Thanks, I understand your example now.

@ArtemG

1 only makes sense if we indeed are pursuing QTT semantics. You mention that that is not a goal in and of itself and that the delta check indeed is not related to QTT right now. So I will drop that line of defense as it seems irrelevant whether we are close to QTT or not.

Aye, I would not describe “implementing a form of QTT” as the goal – QTT (per e.g. the introduction in the paper) is primarily designed to facilitate tracking the computational use of data at the type level in order to enable generation of more efficient code, avoidance of expensive garbage collection algorithms, etc. – and this is not our goal. To me, our goal is more along the lines of “provide a flexible, efficient linear logic for updating atomic pieces of state [resources] in atomic transactions as a base level on top of which higher level abstractions can be built”.

To this end, @mariari’s concerns are certainly relevant, but similarity to QTT or lack thereof is not a good reason to make a particular decision here, I think. Perhaps it would be worthwhile to try to formalize a wee bit more the logic which we do have, compare alternative versions (e.g. the current version, your proposal, and perhaps some of the alternatives discussed here), formulate more clearly some of the layers which we would like to build on top (e.g. Anoma-level), and only then attempt a more final decision. Given that it’s possible to build the behavior which @mariari wants on top of the RM as it exists right now, I hesitate to change that design (especially in large ways) until we have a very clear idea of exactly what we want instead and why.

[ArtemG]

It is true that amount information would not necessarily need to be stored in value with this proposal, it could be stored elsewhere, but if it affects fungibility (i.e. included in the delta preimage in the linearity check), then a developer must implement a separate linearity check as I have described – and my understanding of this proposal is that everything in a resource affects fungibility, so that would entail this requirement.

I don’t think I have quite made myself clear enough here, I apologize, let me try to rephrase this. From what I understand, the “linearity check” you mention comes from implementing amount checking in resource logics instead of in delta proofs, as per the examples in one of your former threads. Now, what I am saying is that this is the exact proposal of @mariari’s, to which I am trying to tailor my proposal. Hence it is strictly speaking not a concern to be placed in this proposal but @mariari’s it seems.

Hopefully I did not misunderstand, but judging by the CL AL codebase that’s exactly what is currently happening.

Homomorphic commitment addition simply allows a third party to add (or subtract) commitments without knowing their preimages

I understand what being homomorphic usually means over some object with some operation such as “+” What I do not understand is why there needs to be any additional homomorphism on top of the one granted by e.g. Pedersen commitment scheme.

But again I sadly do not see how exactly it deals specifically with my proposal rather than the general approach of tracking amounts of resources through resource logics.

To me, our goal is more along the lines of “provide a flexible, efficient linear logic for updating atomic pieces of state [resources] in atomic transactions as a base level on top of which higher level abstractions can be built”.

Right, the only problem here is figuring out what “efficient linear logic” is. It can mean very different things to whoever you say that to. If you really want something like that, you probably would want to say something akin to “there exists a TT into which Linear Type Theory embeds for which a derivation can be interpreted as a valid RM transaction”.

However, here we may come to a problem: I personally currently do not know of a Type Theory that implements a quantity-tracking over types like you describe corresponding to our current delta check. There may be and it would then be really cool to model it!

Otherwise saying that current delta proofs are somehow implementing a linear logic is I think a bit of a misleading statement. They do not seem to correspond to any variant of Linear Type Theory property I know, although here of course I may just be ignorant.

On the other hand here I may just be over-concentrating on the usage of terms. It just seems to me that you want RM to have some properties that do indeed correspond to linear logic, in which case you need an actual linear logic to claim connection to. However, if we do not claim actual connections to linear logic, then there is no problem.

Perhaps it would be worthwhile to try to formalize a wee bit more the logic which we do have

Yes, I think this is a worthwhile task if we accept my point above.

Again, that is not to say that the delta check does not serve a role currently, it does, it is just hard to make any concrete claim regarding its connection to “linearity” in the type-theoretic sense if we indeed want to have that kind of correspondence.

Given that it’s possible to build the behavior which @mariari wants on top of the RM as it exists right now, I hesitate to change that design (especially in large ways) until we have a very clear idea of exactly what we want instead and why.

I absolutely agree with you here. This is why it is merely a proposal. It bears a lot of presuppositions. I also agree that we first need to see what @mariari can cook up for AL specifically before making appropriate changes on the RM level and only get rid of those issues which pose a fundamental problem to the design.

Generally speaking, I am fine with keeping the design as is. I am here trying to grasp several concerns and propose a possible solution, the concerns being e.g. we want to track amounts of things with supply in values, we want quantity field to have a connection to some sort of a linear logic, etc

[cwgoes]

As a note after discussing with @mariari: I think the strongest argument in favor of this proposal is that we might be able to eliminate the delta-check and computation altogether, since in order to check unique resources being created/consumed in the appropriate fashion you simply need to check commitment and nullifier inclusion and correspondence, there’s no need for a “linear” check like delta.

Eliminating the delta concept and computation would be a substantial simplification to the base RM. I have not thought through all of this yet but it’s worth working out in detail.

[cwgoes]

@ArtemG

I don’t think I have quite made myself clear enough here, I apologize, let me try to rephrase this. From what I understand, the “linearity check” you mention comes from implementing amount checking in resource logics instead of in delta proofs, as per the examples in one of your former threads. Now, what I am saying is that this is the exact proposal of @mariari’s, to which I am trying to tailor my proposal. Hence it is strictly speaking not a concern to be placed in this proposal but @mariari’s it seems.

Ah, I see the distinction you mean now – yes, indeed.

@ArtemG

Otherwise saying that current delta proofs are somehow implementing a linear logic is I think a bit of a misleading statement. They do not seem to correspond to any variant of Linear Type Theory property I know, although here of course I may just be ignorant.

On the other hand here I may just be over-concentrating on the usage of terms. It just seems to me that you want RM to have some properties that do indeed correspond to linear logic, in which case you need an actual linear logic to claim connection to. However, if we do not claim actual connections to linear logic, then there is no problem.

@ArtemG

Again, that is not to say that the delta check does not serve a role currently, it does, it is just hard to make any concrete claim regarding its connection to “linearity” in the type-theoretic sense if we indeed want to have that kind of correspondence.

Fair. Luckily I think we may indeed be able to formulate what is it that we’re attempting to do here clearly as a logic, and if not, then perhaps there are parts of it which we don’t fully understand (and should). More to be discussed in the meeting tomorrow.

[xuyang]

If I understand correctly, the main argument is that if we should move the balance check to the application resource logic and if we need to redefine the delta proof and quantity.

It makes sense for applications to define their own balance checks, but privacy and zk proofs may introduce complications. The logic circuit can only access resources in current action, so we have to ensure the balance by creating or consuming ephemeral resources/logic in each action to connect different actions, as @mariari demonstrated in his example. And he already noticed that we cannot put key info to value of ephemeral resources. I believe his approach works but complicate the balance checks slightly. That’s why we decided to separated and unified the delta proof (formerly called binding signature) in shielded RMs, similar to Zcash and MASP. This reduces implementation risks and allows developers to focus on application constraints rather than common balance checks, though it sacrifices some flexibility. We assumed zk circuit design and implementation were not trivial. With zkvm and DSLs, this may no longer be true? I don’t know.

Additionally, keeping the current delta proof (kind-quantity homomorphic commitments) might help with interoperability. Resource structures(element types, hashes, etc.) and logic depend on VMs and proving systems, but the delta proof can bridge differences between RMs without unifying all types and hashes. For example, the “XAN” resource in RM1 and RM2 are of the same kind in reality, but the computed kinds are apparently distinct as they are implemented in different RMs. The core idea is to explicitly make “XAN” in RM1 and RM2 convertible in the delta proof. This approach is still immature though.

[vveiln]

@ArtemG

do we ever really care that a non-ephemeral resource has some local linearity using semantics described by, again, Jeremy’s post? The answer to me seemed to be “no”.

If I understand the definitions correctly, I think I disagree. Example: transfers, but there we consume first to create, not the other way around (like for intent resources). The proposal doesn’t seem to work in that case.

[ArtemG]

For example, the “XAN” resource in RM1 and RM2 are of the same kind in reality, but the computed kinds are apparently distinct as they are implemented in different RMs. The core idea is to explicitly make “XAN” in RM1 and RM2 convertible in the delta proof. This approach is still immature though.

So as I mentioned during our meetup this does seem like a great approach! However that still requires a lot of presuppositions for the current system, i.e. that the labels e.g. are of the same size for both RMs and that the logics are compiled the same.

Currently neither is the case for e.g. transparent and CairoRM. So I do think that having this kind of interop would be great and if it is specifically our delta system that allows it it would be the perfect argument against the approach, yet I do not see it being the case via the current design.

[ArtemG]

Example: transfers, but there we consume first to create, not the other way around (like for intent resources). The proposal doesn’t seem to work in that case.

I do not think I fully understand the problem here, sadly. It is not a priority but when you have the time, I would be interested if you could elaborate on this. Thanks beforehand!

[vveiln]

Intent resources: the user creates (1) the resource first and when the intent is satisfied, the resource is consumed (2)

For transfers, the user consumes (1) the resource first, and then “the same” resource is created (2) for another owner, all in the same transaction.

By transfer I mean consuming a resource and creating “the same” resource, possibly with some fields like value changed. They should balance locally, but they are the same only on the higher abstraction level.

@ArtemG

The answer to me seemed to be “no”. We only care about local linearity if we have some intent-bearing resource onboard.

For transfers, we care about local linearity and we don’t have to involve intents. Transfers can balance within the same action or across actions as well.

@ArtemG

In other words, things that we care locally (i.e. in terms of local linearity) are exactly things which trigger intents logics.

So this statement seems to be false because we do care about local linearity for transfers

[ArtemG]

@vveiln

Intent resources: the user creates (1) the resource first and when the intent is satisfied, the resource is consumed (2)

For transfers, the user consumes (1) the resource first, and then “the same” resource is created (2) for another owner, all in the same transaction.

By transfer I mean consuming a resource and creating “the same” resource, possibly with some fields like value changed. They should balance locally, but they are the same only on the higher abstraction level.

Hm I apologize, I still do not quite see how this goes against the current proposal. Is the problem that you claim that such a transaction is not balanced in my presentation? In the vocabulary I used, these stand for proper resources we care about globally and hence, here I quote myself:

@ArtemG

Usual resources we care about globally (like XAN, spacebucks, whatever) have 0-quantity.

In other words both resource 1 and 2 (which are of course different resources as they have different owner) are not used in the delta proof as both of their quantities is 0. So if there is e.g. a transaction with only these two resources in it is will pass the balance check using my presentation.

Or did you mean something else?

@vveiln

So this statement seems to be false because we do care about local linearity for transfers

Ok, here I think maybe I jumped the gun in trying to get rid of ephemeral resources. I think I actually have a formal claim behind it, which is: “the set of valid transactions for the current RM is in bijection with the set of valid transactions of the RM + my proposed changes”

However I of course have not properly proven it or showcased it yet, so it is fine to have general arguments for/against this on a higher level.

Nevertheless, as I mention in my original post:

@ArtemG

If I am not mistaken Jeremy’s issue can also be fixed using only the last part 3 of my proposal. Namely make deltas account for the entire resource sans quantity. The ephemerality removal jumps at me though as the next logical step due to the prior discussion.

So for the purposes of the discussion I think it is best to think of the core of the proposal as changing the delta preimage keys rather than anything to do with ephemeral resources.

[xuyang]

However that still requires a lot of presuppositions for the current system, i.e. that the labels e.g. are of the same size for both RMs and that the logics are compiled the same.

Yes, it does require some presuppositions. However, we don’t need to unify labels and logic for different RMs. Each RM can retain its current design while achieving interoperability. This is what I personally expect to see. It also depends on how we define the interoperability. Ideally, we only need to add a few features to the current delta proofs to make resources in different RMs convertible. This approach relies on the current kind-quantity homomorphic schema and checking the balance at the transaction level as it is now instead of checking it app logic in this proposal. Many details remain to be finalized, and I’m unsure if this will ultimately meet our requirements.