Let us talk about intent bearing resources and the issue with the value field.
In particular I will approach this problem as a compiler developer who wishes to target the resource machine, meaning that I generally have a model of how I compile to resources, actions, and transactions.
A lay of the Meta Model
In this model I’m creating, I’m compiling objects to resources, and operations over objects into actions or transactions depending.
I compile objects to resources simply… I map the instance slots to the value slot/field. I store the class name to the label so that I can fetch data in the transaction function to get fields shared across all instances.
Using this I can compile all objects of a given system into a valid RM resource. Further, operations which are partially applied (let’s say we want to swap A for B, but we only have A), compile to intent bearing resources. The specifics of this process do not matter for this discussion.
Further I do not use the quantity field of the RM at all outside of setting it to 1 for the sake of this post. Thus when quantity is mentioned it is solely in context to values stored in the value or label field/slot.
Spacebucks
Now that we got the preamble out of the way, I can introduce the spacebuck resource.
;; For those not allergic to parens
(defclass spacebucks (ownership-mixin fixed-supply-mixin) ())
A spacebuck is simply a resource that is madeup of 2 properties:
There is a fixed supply of spacebucks people can not arbitrary mint nor burn spacebucks
Spacebucks have an owner, in such they can be owned by some identity/private key.
For the sake of this analysis, I want to highlight property 1. and mostly ignore the concrete details of property 2..
We can implement property 1 as follows:
In the resource logic of any spacebuck resource the resource logic will only return true iff there exist another ephemeral resource, let us call this resource FixedSupply, in the same action as it.
FixedSupply has the label containing the quantity corresponding to the resource in 1..
FixedSupply has the logic that when created it unconditionally returns true. When consumed this resource checks that the number of the spacebucks has either been minted (if the spacebuck in 1. is burned) or burned (if the spacebuck in 1. is minted).
Now let us imagine an operation where we simply give away the spacebucks to anyone who wishes to claim it.
In this scenario, we create an action simply burning our spacebucks. In this action we have the FixedSupply intent bearing resource. Someone who wishes to claim this spacebucks must consume this FixedSupply with kind K in their own action if they wish to pass the delta balance check.
In doing so, the FixedSupply check goes off and ensures in this second action that the same number of spacebucks are now minted to the claiming party.
The Issue
Now imagine if I implemented the FixedSupply and spacebucks example above, putting the amount in the value slot/field of the FixedSupply intent-bearing resource. In that scenario, the person claiming, can simply modify the value slot to have 10000000000 spacebucks. Now the FixedSupply consults the value field, and in this case if the claiming party mints 10000000000 spacebucks then everything will pass. This is because in this scenario the kind K does not change, and since the resource logic refers to the value, the claiming party can simply change the data and mint as much as they want.
This is a huge problem, and thus we must put the quantity in the label so it can affect the kind. This however from a compilers POV is a problem because in most every scenario I can use the strategy where the value slot/field is a standin for instance variables, and the label for the class, however in this scenario the value field is completely compromised and is instead an active footgun to avoid at all costs. In particular, this means the compiler developer for this particular part of the RM should pun the label field for the old meaning + the new meaning and hope this doesn’t ruin the semantics of their mapping.
I can see a few problems with how this application logic is defined.
You mix up different resource logics. You use FixedSupply resource to both ensure that the supply is fixed and to let the user to express their intent, and on top of that, it is done in a way that the first action balances the second action. You can see it is inconsistent even from the naming. It is called FixedSupply but you refer to it as intent bearing resource, which is impossible to infer from the name. The name is supposed to reflect the function (all the functions), but it doesn’t.
If you have constraints about what the user can demand, you have to verify the constraints. You say that the user can arbitrarily change the value and it balances the transaction - yes, because you designed the application in a way that allows the user to satisfy a different logic by stating their intent and do not verify what they ask for while actually having implicit constraints on that.
Here is how I would design this application
1. Terminology check
Mint = create persistent resources, consume the same quantity of ephemeral resources.
Burn = consume persistent resources, create the same quantity of ephemeral resources.
Transfer = consume persistent resources, create the same quantity of persistent resources.
2. Fixed supply spacebucks
The idea is simple: we mint all of the spacebucks in the very first spacebucks transaction and after that only allow transfers (no ephemeral spacebuck resources). The challenge is how to ensure that this mint transaction happened only once. Since a single transaction doesn’t have the history of state changes in its context, we have to rely on some external source of information for that. For our simple version, we assume that there is a controlling entity that has to authorise the very first mint transaction and will not authorise such a mint transaction ever again. We trust to controlling entity for that.
Now that we have our spacebucks, allowing only transfers (no mint or burn) automatically ensures our supply is fixed.
3. Spacebuck giveaway
The user expresses their intent. I would naturally express it in the logic field, but to follow your value approach, let’s do that. The spacebuck-giveaway-intent logic works as follows:
Create spacebuck-giveaway-intent resource: always true. The resource contains in the value how many spacebucks they want + the user identity.
Consume spacebuck-giveaway-intent resource: only happens if the same action contains if (let’s assume for simplicity that value only contains the number of claimed spacebucks) spacebuck-giveaway-intent-resource.consumed.value = spacebuck.created.value (and check the owner too, but I omit that). We don’t actually care what the value of the spacebuck-giveaway consumed (balancing) resource will be, but we can also explicitly verify the correspondence in the logic, if we wish to.
4. Ways to simplify
This is not so relevant to the topic, but I have to mention.
In this particular design, the user doesn’t even need to use intent resources for that. They can just go ahead and create spacebucks for themselves and this transaction will only balance if someone consumes their spacebuck resources since only transfers are allowed.
5. Takeaways
Resources are the only way to bind the correct predicate satisfaction to the validity of the transaction. We can’t ensure that some arbitrary predicate is satisfied if it isn’t a logic of some resource.
Do not rely on balance to verify constraints. Transaction should only balance when the constraints are satisfied, but balance itself doesn’t verify the constraints, logics do.
Every constraint you have in mind must be explicitly verified by the logic. The good news is that every logic has access to every resource object in the same action.
The shorthand example I gave was made for minimalitiy to show the issue of placing data in the labels, it wasn’t meant to tell the full story of what will happen, namely some sketches of techniques as the full story complicates the story with details unnecessary to the issue at hand.
In reality in the code that I have worked out, when the user has some intent, this would not be carried out by the FixedSupply, instead it’ll be an additional intent bearing resource.
In particular I imagine it like this
(defclass fixed-supply-mixin ()
((supply-quantity :initarg :supply-quantity
:accessor quantity :type integer)
;; One argument not given due to it being an implementation detail unrelated to anything at hand
(:documentation "I maintain the invariant that things are of a fixed supply"))
(defclass fixed-supply-intent ()
((quantity :initarg :quantity :accessor quantity :type integer)
(class-assurance :initarg :class-assurance :accessor class-assurance :type symbol)
(should-create? :initarg :should-create? :accessor should-create? :type boolean))
(:documentation
"I represent an intent that assures fixed supply is maintained for a particular class.
In particular I assure that x number of tokens are created or burned"))
Here we have 2 classes, these will both map to resources, the first is the fixed-supply-mixin, the point of this is to mix it into something you’d actually use, not use it itself.
The second class is the fixed-supply-intent which is what I’ve been calling the FixedSupply intent bearing resource.
Note the code interfaces I’ll be showing below don’t adhere to the RM spec, I know how they map, but if my interfaces are off a bit, I apologize the point is for rapid prototyping as long as strategies are known, adhereing proper would take more time than it’s worth for little gains esp if I know how to map it faithfully. So consider the particulars a bit fantastical but real in execution given some minor mapping back to reality.
For the fixed-supply-mixin if you mix it in, this logic will run along with whatever resource-logic is defined for the actual class used (I.E. spacebucks’s custom logic will run then be anded with this).
This checks that the kind for fixed-supply-intent is in and that the parameters that we expect are adhere to. This just sees if it’s included. Meaning that if anything that mixins in this mixin, there must exist the fixed-supply-intent (side note, I probably should allow user classes to change this with a protocol later…). This is not the full intent bearing resource, when operations are done, there will likely be many intent bearing resources that will fall out that some other action must nullify.
Now for the reosurce logic for the fixed-supply-intent
Here, this resource logic returns true if it’s not being consumed, if it is being consumed then we check if the exact number of resources are either being created or destroyed
I believe our designs here are the same, I don’t include any identity information in my code above, as I’d get this from the ownership-mixin, I view this as a separation of concerns that is important for spacebucks and can be automatically derived for it
The intent is needed here, as I’m specifically not punning the number of spacebucks to the quantity. I.E. 5 spacebucks makes a quantity of 1. I want to show that we can rest on the delta balance being for linearity with zero punning required, but we can pun for efficiencies
I believe we are both in agreement, in fact I believe the design I’m going for with all the mixins basically does do this, as we will create extra functions to be checked for your point 4.
If you wish to read the prototype code I have it’s here:
As the code currently stands, I’m not happy with it, it’s still far too low level (read too close to the RM), I know some techniques that can make the interface seem much higher level and make writing to the RM more intuitive and easy from a user POV. I will continue developing this until I make a simplified version of multi-chat along the way refining the interface until I think it’s actually intuitive to write.
Once that happens I plan on making some AL demos in our Anoma codebase and begin that process.
Let me know what you think of the code, I can walk you through the machinery behind it and why I made certain design decisions
I generally agree with that, but it doesn’t help to see the problem if you show it on an example that doesn’t make sense in reality. If there is a way to solve the problem by realising that the case in which it occurs never happens in practice, I usually go for that over solving the problem that will never arise.
It makes sense to me, but do we actually want to always do that? In this particular case it makes sense to take advantage of the semantics. Although I understand that it is also just an example.
But do I understand correctly that the issue you pointed out is solved fine with validating the value + ensuring fixed supply by only allowing transfers? Ensuring fixed supply via transfers is specific to this case, but validating the value of the desired resource in the logic (if not for direct value, then for the value relationship, e.g., “value of this resource is the same as the value of that resource”) is not and it seems to me that it solves the problem. Or am I missing something?
We want to show that it’s possible to do everything without resorting to abusing the semantics to pun the meaning of linearity. In particular this case demonstrates something that needs to be clarified in the current RM: “If we don’t pun the meaning, then we run into an issue where for trying to uphold any global property P', we can do it by making an intent bearing resource where all the value field slots are in the label”. Punning the Delta check means that this bit of exploration would have be found much later.
Further, I fear if we try to pun and abuse semantics at this level, it will leak through the model. I have to as the user know that “ahh yeah it’s best I say this slot/field should be mapped to an underlying quantity field in the RM”, meaning one has to be taken out of the higher level object system for a hard requirement. Likewise for the intent bearing resource, with no changes, the developer will have to say “Yes… I have to declare all these fields must be mapped down to the label field/slot…”. Ideally the user doesn’t have to think too much about the machinery of the RM, just of some properties they wish to hold.
Yes the technique solves the problem, the issue is what the OP is about, namely that we have to magically know what I’ve been putting in the value field/slot needs to go into the label. Further the value field becomes a footgun in this case as it’s completely untrusted for it’s purpose and should be avoided.
To use something for two purposes at once. I.E. use linearity both for linearity checking and punning it to also do something unrelated like token balance checking
Isn’t linearity ensured separately, by the commitment-nullifier mechanism?
I would say the difference between putting something in the value vs putting something in the quantity is if you want to use the balance check mechanism for enforcement or not. The difference between validating something in the logic vs validating something by binding it to the balance check is the scope: balance check’s scope is transaction (so it allows for intra-action constraints), logic’s scope is action.
We can propose a standard and explicit way when to use one or the other, if it helps.
Why does it have to go to the label? The solution doesn’t require that, you just need to validate what is in the value field.
How do I validate that? Would this require me to sign over some data? If that’s the case then it takes a lot more to work to try to get it there (I.E. we have to have some key and ownership along with the signature). Are there cleaner ways to validate the value field?
That is the linearity mechanism for specific resources, but over transactions themselves the quantity field becomes the linearity marker
The balance check a particular global property you want, yes, however it’s not a fully general mechanism and of limited use. We can thankfully get this global property using resource logics meaning that we can use the balance check strictly as an optimization, not a necessity to get global (to a transaction) properties.
No, as I can understand where it can be useful, however I don’t think is a detail that should be pressing at the users minds when they design objects. I.E. I fear this will leak into the semantics of the object system forcing programmers to program at far too low of a level (if they do understand and want to look under and change how the mapping works they are free to do so, but this should be an optional thing, and something the standard library can help make fast by doing the faster thing when composing itself).
Most likely by constraining it to be equal to another value, e.g., consumed.value = created.value
Often you don’t care about the exact value, you care about the relationship between the value of one resource and some other field of the other resource.
No signatures involved
I’m not sure what you mean by linearity over transactions
Isn’t it kinda..problematic that you decide to go around the intended behaviour? If you think balance check is useless, it is a question to raise in the spec context, but discarding it like that feels like a suboptimal practice.
But these are in different actions, so I can’t do that here! The kind balancing (linearity) here enforces that this intent-bearing-resource must be included and thus allowing this to be consumed in a separate action in which the original value is out of scope.
the quantity check is linearity over the kinds within a transaction
I never claimed the balance check is useless, it serves a key point in making the system function, I.E. that you have balancing of kinds (linearity on kinds). When I asked @cwgoes about the purpose of the quantity he said that it comes from linear logic. The issue I’m bringing up is much more general than a quantity check, as it’s a much more limited device and if that is the only way we can guarantee some global property then we will run into issues. To summarize the benefits of the approach I’m going for:
It shows that we can ensure global properties throughout the transaction
It shows that we can use a clean mapping from objects<->resources where limited special casing is had
By avoiding excess special casing we avoid the machinery around the RM from leaking into developers code causing them to only care about the main properties they wish to ensure.
However in realizing a conceptually easy model to run we run into the issue of the thread:
As it currently stands in the case of an intent-bearing-resource the value field is only a footgun, and all data in this one instance has to be moved to the labels. There have been some solutions proposed by @cwgoes however I’m looking forward to seeing an exploration of the solution space for this particular issue.
Ah, I see what you mean. Then yeah, it has to be bound through the logic/value, which is a problem if you want to use value to specify your intent. What is the problem with specifying it in the logic directly? That is how we imagine it usually, a predicate.
I can conclude that value is only useful within the same action and cannot carry intent information unless there is a cross-action enforcement mechanism. This mechanism should be optional (i.e., we don’t want to enforce it for all resources with certain properties)
Do you have ideas about other ways to guarantee global properties that would not suffer from the same issues? I mean on the design level, e.g., if we can add something like quantity field but more general. What properties would this field need to have to make things easier?
The problem would be that this is bespoke per spacebucks here. Namely for every parameter that goes in the value we have to include it in the logic directly or the label, which circles us around to the problem described above.
Yeah this is what I’m interested in seeing, it’s clear we can’t blanket add this mechanism to all ephemeral resources.
Well the quantity mechansim on it’s own can’t guarantee us arbitrary global properties, however when we use this along with the intent-bearing-resource strategy with values fixed in the label. Then we can use these to guarantee global properties via resource logic across actions. Thus the quantity mechanism used in this limited way acts as a linearity check for resources across actions. Thus we can get the property such as getting a stable supply of a token through the linearity properties of quantity. We could also use quantity in a different way such that the number of tokens goes with the quantity, this is fine and even more optimal for this use case however it’s more limited in it’s applicability for ensuring global properties. Either way I’m happy with this mechanism now. I think the main thing I want is to just get ideas going on value mechanism within the intent-bearing-resource. I hope that makes sense?
I’ve got an impression that you were explicitly not happy with carrying the intent in the logic/label and wanted a way to do that in the value. If you are happy, then the solution is simple: don’t use value for specifying across-action constraints.
I want to put it in the value, hence the thread, I’m happy with the general mechanism just not where the data has to go here and I would like some designs around this potentially
You might have answered it somewhere in the thread already, but I’ll ask again to understand the situation better: why do you want it to be in the value? I assume it must be because you don’t want to affect the resource kind. Is there a reason for that?
The kind for each resources is potentially different…
This means if you are trying to make intent-bearing-resources combine with other intent-bearing-resources to potentially balance out (like a delta balance of 1 + -1 = 0), then you have to filter on resources based on their resource-logic field instead and do some calculations on their label values.
All of this is fine, and I don’t mind it, I’m not sure if you do however.
This is the only case that I’ve found so far where I have to be unprincipled in my mapping down from objects to resources. I have been using the label as a particular semantic meaning which has great value, but in this one scenario only I must move all the value field/slots into the label field alongside my original design. This has some unintended consequences that leak to the users of the system
I think the fact that we have different kinds for different intents is fine. It feels a bit counterintuitive, but I don’t see any actual issues with that aspect
What if you move them not to label, but logic? It makes sense to me semantically, but I can imagine it might sound even worse to you.
Intent carrying resources are a bit of a special case. Do you think it could make sense to separate on the language level between different classes of resources? I can see 5 different classes:
persistent non-zero quantity
persistent zero quantity
ephemeral zero quantity resources
ephemeral non-zero quantity resources,
ephemeral non-zero quantity balanced across actions (intent carrying resources)
These classes do not perfectly partition the space of resources (specifically, the last one is a subset of the fourth one), but since they all serve different purposes, maybe it makes sense to branch on the language level.
point 1. in my last post is no longer possible, since you can’t even check the logic is the same.
You can no longer inspect on the data, they are all stuck in a lambda and thus there is no way to access the values from another resource logic
Maybe, but a straight mapping directly from these categories into the model will add a lot of complexity to the language and make the language challenging to use and learn. Thankfully I think it can be done in smarter ways where it is shown in a way that people can already understand and doesn’t bleed heavily into the higher level semantics of the language.
One thing I’ve found it that most computations aren’t real. Namely, objects like 1 map down to being the resource 1, however since they pose no global constraints they safely can be zero quantity ephemeral resources. A lot of objects will be like this covering the ephemeral zero quantity resource case.
Another example is that I want to break down the resource-logic into 3 different methods (one which must always hold about the data to be a valid instance of a particular object, one that happens on creation and one that happens on usage), which reshifts the resource logic into a way that is intuitively familiar.
Direct knowledge of the RM will help in designing the system smartly, as one can learn how to do faster patterns, however I hope it to be like learning what is fast for underlying hardware and have it be something people can ease into learning (I want to make tools in aiding this process).
I think so far I’ve discovered
ephemeral zero quantity resources
ephemeral non-zero quantity balanced across actions (intent carrying resources)
persistent non-zero quantity
However, how do you see:
persistent zero quantity
ephemeral non-zero quantity resources (other cases of this)
being used? I’d be interested, as I want to digest all of these naturally into the meta-model I’m creating.
I think the model is a success if we can digest all use cases without having the language be:
Having a huge complexity floor (mind you the language is general and supports writing things like engines and basically bootstrapping the entire Anoma OS, so it will be interesting and something somewhat unfamiliar for others)
Having programmers program at the resource level
Having a lot of code to make programs work (writing code for all the various resources needed for this. Such examples are multi-chat and kudos).
I believe being able to put the data for an ephemeral non-zero quantity balanced across actions in the value will help on this mapping and avoid the semantics from leaking to the language (causing a higher complexity floor) as the only way to do this that I can see is by having some class C that is an intent-bearing-resource that all intent-bearing-resources must inherit from rather than the base standard object that everyone else does. Meaning it’s just one more thing a user can mess up and must keep in mind when designing things (You can’t simply hide this, it will show up somewhere in the object model as even the RM is reified in language to allow users to better understand the mapping and control it themselves when they want to.)
Minor note: the label must store a binding class name (e.g. a hash of the class logic or something), otherwise someone could simply insert different class logic in the transaction function.
I think we may be bundling two conceptually distinct choices into the “ephemeral” flag at present:
The choice of whether a resource should have been created prior to this transaction or within it, and
The choice of whether a consumed resource should have been created “from nothing” (i.e. commitment existence is not checked) or whether it should have been created at some point beforehand.
Namely, right now we have the choice between:
Non-ephemeral resources, which must have been created before the transaction in order to be consumed (and included in some past commitment tree root), and
Ephemeral resources, which can be created and consumed in the same transaction, but for which commitment existence is not checked.
As far as I can tell, we don’t have the ability to demarcate a type of resource which should be created and consumed in the same transaction and where commitment existence is checked. I think that this ability would be useful – not just for @mariari’s goals here, but also more generally.
To me, consuming resources that were never created before is really a special tool – in a sense, the boundary conditions of a linear logic – that should be used only for the purpose of introducing resources “out of nothing” from an application semantics perspective (such as newly created kudos) or vaporizing resources “into nothing” from an application semantics perspective (such as burning kudos) – it shouldn’t really be used for constraint-carrying.
I have a wee proposal that I think might reconcile our goals here:
Split the “ephemeral” flag into a triple. Resource “ephemerality” can be either “spontaneous”, “transient”, or “persistent”. Both “spontaneous” and “transient” resources are ephemeral in the sense that they have no lifetime beyond a single transaction. “Persistent” resources behave as regular (non-ephemeral) resources do at present.
“Spontaneous” resources are handled as “ephemeral resources” are currently.
Commitments of “transient” resources are added to a temporary commitment tree and nullifiers of “transient” resources are added to a temporary nullifier set. In the transaction validity check, check that (a) all transient resources consumed in this transaction were indeed created in this transaction and (b) all transient resources created in this transaction were indeed consumed in this transaction.
We would then use “transient” resources for constraint-carrying purposes (such as the one which @mariari has in mind here), so that value would be checked.