Proposal: Towards QTT Semantics of RM

Resource Machine Stuff
6

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!