Proposal: Towards QTT Semantics of RM

[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.