Proposal: Towards QTT Semantics of RM

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