Table of Contents
- Preliminary Results from the first OO-RM
- Preamble
- Goals Non Goals and Motivation
- The Programming Model
- Imagining a Logtalk Implementation
- The Meta Language Requirements
- Conclusion
Preliminary Results from the first OO-RM
Preamble
Hello everyone I’ve doing some experimentation on mapping objects down to resources. This is a report from some of the things that I’ve found during this process.
All the code from this post can be found below.
https://github.com/anoma/cl-rm
Goals Non Goals and Motivation
The main goal of the project is to find a mapping from objects to resources and how operations relate to compiling down to transactions. In particular we expect that all objects can be mapped down to resources. Further we’d like to explore what objects that are specifically designed for the resource machine would look like and want to create idioms that allow us to take into account that we do not have all the data upfront.
A non goal is having the prototype code be specs compliant, it is sufficient that we understand how the code could be implemented in a specs compliant way. The rational is that making it specs compliant off the bat only slows down exploration which is the key element we are optimizing for.
An important style of design that we wish to achieve is one that allows users to have full control of the system if need be, but offer a good all around solution that is fit for the vast majority of use cases. This can be done by making various layers of abstractions that layer ontop of each other and most importantly can access fully the lower layers when convenient. As instead of a strict layer separation strategy of moving all the components together in batch, we instead open up all layers along this chain as an API so the layers above can skip to a more efficient section if it suits them. Since all of this work is reified in the system, the user can also utilize this to create faster applications.
A future direction to take this work is to research how meta objects relate to this compilation procedure and how changing our fixed point of the object system within common lisp may be beneficial for compiling things such as intent carrying resources.
The Programming Model
Base Level Mapping
The very first layer of the work can be found in the cl-rm folder. This includes the base model along with some environments. Let us first focus on the first layer of work to get meta model working.
The very first thing I do is model the data types for resources, instance and compliance unit
https://github.com/anoma/cl-rm/blob/400c1775c0360f2428c90e2325697066797a621c/src/cl-rm/cl-rm.lisp#L8
(defclass resource ()
((label ...)
(data ...)
(quantity ...)
(nonce ...)
...))
(defclass instance ()
((tag :initarg :tag :accessor tag :initform nil)
...)
(:documentation "A not very accurate instance"))
(defclass compliance-unit ()
((proof :initarg :proof :accessor proof :initform nil)
(vk :initarg :verifying-key :accessor verifying-key :initform nil)
(instances :initarg :instances :accessor instances :initform nil))
(:documentation "In a transparent case the only real field is instance"))
The only somewhat accurate type to the specs is resource. compliance-unit is what I’m using as a singular action, which like instance is not very accurate to the specs. However they are accurate in the sense that they contain all the information that is had when a resource-logic is run and are thus admissible for this prototype.
As of the time of this writing we have not modeled transactions. However further work on this front is wanted but for the initial exploration this was not strictly required.
(defclass method-resource ()
;; type is funcallable to be more accurate.
;; If we have more outputs, then we'd care about that as a field
((gf :initarg :gf :accessor gf :type symbol)
(num-args :initarg :num-args :accessor num-args :type fixnum)))
Before we move onto the various protocols that let the machinery work, let us look at the method-resource type. This type simple is a wrapper type over a method application, we simply track the number of arguments the operation took and the function itself. For example:
(+ 1 2 3 4 5)
Would compile down to
(make-instance 'method-resource :gf #'+ :num-args 5)
Protocols
We shall now dive down into the protocols of the system, these are various methods (generic function in CL parlance) that allow us various parts of the machinery work.
Each section will the generic functions purpose in the whole and give some examples of their usage.
Object↔Resource Transformation
This protocol is important as it controls how objects map down to resources and get mapped back, let us look at the methods
(defgeneric obj->resource (object)
(:documentation "I turn an object into a resource"))
(-> resource->obj ((or null resource)) t)
(defun resource->obj (x) ...)
These functions are obj->resource and resource->obj. The names are self explanatory. Let us look at the implementations of these functions
(defmethod obj->resource ((x standard-object))
(let ((class (class-of x)))
(make-instance
'resource
:data (cl-rm.utils:instance-values x)
:logic #'resource-logic
;; Label is a reference to the slot values that we need to refer
;; to, however since we recreate the value and the data is
;; available Ill elide this detail, what we want is to basically
;; have a reference to the specific class values in some way
;; which can change, not sure what this looks like. However we
;; can always retrieve the class this way
:label class)))
(defmethod obj->resource ((x number))
(make-instance 'resource :data (list x)
:logic #'resource-logic
:label 'built-in-class))
(-> resource->obj ((or null resource)) t)
(defun resource->obj (x)
(when x
(case (label x)
(built-in-class
(car (data x)))
(t
(cl-rm.utils:list-to-class (c2mop:ensure-finalized (label x))
(data x))))))
When we map down any user defined class it by default goes through obj->resource, which simply shoves the slots (fields to those from Java) in the data slot, puts the class in the label (in a real implementation we’d have to be more careful about that detail), and the function #'resource-logic in the logic. Further the class-side slots are not shown here, as they belong to the class. When we run resource-logics this means that we must supply the appropriate value from the class before running our logic in a real implementation.
The #'resource-logic is a generic function, meaning that
TEST> (eq #'resource-logic #'resource-logic)
T
However we can find the specific instance, since we know statically what the first argument is, so this is a perfectly valid shorthand for experimentation.
Going the other way, we can see that we simply use the label to recreate the class with each value in the data being mapped back to the appropriate slots in the allocated object.
Note that resource->obj is poor in that I could still do generic dispatch even though we simply take a resource, by dispatching off the label itself so the user can control resource->obj if they had a custom obj->resource (this is necessary for intent-bearing resources to change how the compilation works).
With that said, let us look at how this works in practice
(defclass integer-obj (cl-rm.mixins:pointwise-mixin)
((data :initarg :data :accessor data :type integer)))
(defclass counted-integer (integer-obj)
((counter :initarg :counter
:accessor counter
:allocation :class
:initform 0)))
(-> mk-integer (integer) integer-obj)
(defun mk-integer (x)
(values (make-instance 'integer-obj :data x)))
(-> counted (integer) counted-integer)
(defun counted (x)
(values (make-instance 'counted-integer :data x)))
TEST> (counted 5)
#<COUNTED-INTEGER 5 0>
TEST> (obj->resource (counted 5))
#<RESOURCE
#<STANDARD-CLASS CL-RM.USER:COUNTED-INTEGER>
(5)
#<STANDARD-GENERIC-FUNCTION CL-RM.GENERICS:RESOURCE-LOGIC (4)>
1
#(0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0)
NIL
NIL
0>
The Three Predicates and It’s Precursor
So we have a mapping between objects and resources, but how do resource logics work and how do we run them?
(defgeneric resource-logic (object instance consumed?)
(:documentation "I run the resource resource-logic for a given type")
(:method ((object standard-object) (instance instance) consumed?)
(and (always-true object)
(if consumed?
(holds-on-use object instance)
(holds-on-intro object instance)))))
(defgeneric always-true (object)
(:documentation "I must always hold for the object to be considered valid")
(:method ((object standard-object))
(cl-rm.utils:subclass-responsibility object)))
(defgeneric holds-on-use (object instances)
(:documentation "The property that must always hold on the object being used")
(:method ((object standard-object) (instance instance))
(cl-rm.utils:subclass-responsibility object)))
(defgeneric holds-on-intro (object instances)
(:documentation "The property that must always hold on the object being created")
(:method ((object standard-object) (instance instance))
(cl-rm.utils:subclass-responsibility object)))
The very base layer of functions being ran is resource-logic. In particular this method is ran on the object representation of the resource, not a raw resource itself. It also takes the instance and whether it’s consumed or not. This is a bit different from the specs but all this information is known during verification time and thus we are perfectly within the realms of what the real RM knows. Also even at this level, before feeding the data into the resource-logic function, we make sure to turn all resources in the instance into an object, as we’ve crossed to the user barrier. With that said I’d argue resource-logic is much too low level, and thus I define the following functions along side it:
- always-true: What must always hold for the object to be considered valid.
- holds-on-use: The property that must always hold on the object being consumed.
- holds-on-intro: The property that must always hold on the object being created.
These three functions more ergonomically bind over the interface as these methods look like normal life cycle functions that state directly what properties must hold under the life cycle of the resource.
Let us continue using the integer-obj type from before
;; Using it in a very low level way
(defmethod resource-logic ((object integer-obj) (instance instance) any)
(integerp (data object)))
;; Using the higher level API
(defmethod holds-on-use ((object integer-obj) (instance instance)) t)
(defmethod holds-on-intro ((object integer-obj) (instance instance)) t)
(defmethod always-true ((object integer-obj))
(integerp (data object)))
TEST> (always-true (counted 5))
T
TEST> (always-true (make-instance 'counted-integer :data "hi"))
NIL
resource-method is a more interesting case, as this is something we’ll need for the actual model to work, let us look at the structure of it’s predicates.
(defmethod always-true ((object method-resource)) t)
(defmethod holds-on-use ((object method-resource) (instance instance)) t)
(defmethod holds-on-intro ((object method-resource) (instance instance))
(cl-rm.utils:obj-equalp
;; We check the output is equal to the work
(cadr (created instance))
;; We assume all inputs are stored next to each other at the start
;; of the consumed
(apply (gf object)
(serapeum:take (num-args object) (consumed instance)))))
resource-method is interesting in that it only cares about checking some property when it’s introduced but does not care about being consumed at all (does this imply it should have quantity 0!?). The check that it makes is to simply check that inside of a compliance unit that the output is equal to the running the method again on the first n arguments of the consumed objects. We assume that the compliance unit/action is very specific with the 2nd item in the created instances being the output and the first n arguments were the arguments it’s ran on.
The point of this is to simply check that the logic is all ran.
In the discussion about the logtalk implementation we will cover how this can be extended towards being an intent method across actions.
Delete/Consumption and Introduction
(defgeneric delete (object)
(:documentation "I delete the given object")
(:method ((object standard-object)) t)
(:method ((n integer)) t)
(:method ((s string)) t))
The last protocol simply deals with consumption of resources and instantiating resources. The delete method by default does nothing, as we typically don’t need to trigger any actions upon consuming a resource. As we can see there is no method (generic function) for instantiation, this is because the functionality is already given by CL under the function initalize-instance.
Meta Environment Protocols
Now that we have all the obvious protocols out of the way, let us explore the compilation environment.
This part is quite crucial, as this ties together being able to emit certain objects that ought to exist whenever we try to form a transaction. In CL we model this imperatively mutating a list in the environment. For you Haskell heads out there, this is isomorphic to having a state monad that you add values into, so this is simply effectful with an IO implementation (づ ◕‿◕ )づ.
https://github.com/anoma/cl-rm/blob/400c1775c0360f2428c90e2325697066797a621c/src/cl-rm/env.lisp
(defclass compilation-environment ()
((consumed :initarg :consumed :accessor consumed :type list :initform nil)
(created :initarg :created :accessor created :type list :initform nil)
(comp-operation :initarg :operation
:accessor operation
:type symbol
:documentation "I am the top level operation that is being compiled")
(transaction-data :initarg :environment
:accessor environment
:type hash-table
;; we have to use fset as we need our slotwise equality
:initform (fset:empty-map)
:documentation "I am included in action app-data,
in particular if you want to include data to a particular resource then
set a map for the resource such that:
env ⟶ (kind resource) → data-to-be-passed in
Non resources can also use it, with their data being pruned before the
transaction is made")))
The environment consists of of 4 parameters, extra resources to be consumed, extra resources to be created, the top level operation we are trying to compile and data that is a supserset of app-data.
We have the following operations on this
(-> put-metadata (compilation-environment t t t) fset:map)
(defun put-metadata (env data key value) ...)
(-> lookup-metadata-table (compilation-environment t) fset:map)
(defun lookup-metadata (env data key) ...)
(-> lookup-metadata (compilation-environment t t) t)
(-> put-private-key (compilation-environment ironclad:ed25519-private-key) fset:map)
(-> lookup-private-key
(compilation-environment ironclad:ed25519-public-key)
(or null ironclad:ed25519-private-key))
(defparameter *environment* (empty-environment)
"I am the current environment for compiling a transaction")
(defun flush-environment ()
(setf *environment* (empty-environment)))
(defun emit-created (object)
(push object (created *environment*)))
(defun emit-consumed (object)
(push object (consumed *environment*)))
The first three operations let us put values into the meta-data over specific-resources. We end up doing this by actually turning the data into a resource to store the data as we will copy that particular meta-data into the instance that is passed to the resource-logic. The internal data structure is a functional map, so the key is most likely a symbol for the particular information one cares about for a given object.
I also offer convince functionality for looking-up and putting in keys, these use the same meta-data functionality, but this is convenient for being able to sign over data inside a compilation environment if a key is available to do so. More on this point in the user stories.
Lastly, I offer emit-created and emit-consumed, these functions simply let the user add various objects to be consumed or created during compilation.
Verification
Before we get into how transactions work, let us look very briefly at the verification function and what convinces they offer to the user.
(-> verify-compliance-unit (compliance-unit) boolean)
(defun verify-compliance-unit (compliance)
(null (failed-compliance-unit compliance)))
(-> failed-compliance-unit (compliance-unit) list)
(defun failed-compliance-unit (compliance)
(let ((instances (instances compliance)))
(remove-if (lambda (instance)
(verify (tag instance) instance (consumed-p instance)))
instances)))
(defmethod verify ((resource resource) (instance instance) consumed?)
;; time for the fun
(assure boolean
(funcall (logic resource)
(resource->obj resource)
(cl-rm.utils:copy-instance instance
:consumed (mapcar #'resource->obj (consumed instance))
:created (mapcar #'resource->obj (created instance)))
consumed?)))
Here, we have our verification logic, the important thing to note about this code is that we turn all resources into objects before we call the resource-logic function. This is important as this lets us operate on the level of objects where it matters.
Transact
With the model’s API specified let us dive into how compilation works.
(defmacro transact (expression &key (keys nil))
;; poor man's stepper
(let ((rest (gensym "CDR")))
`(let ((cl-rm.env:*environment*
(cl-rm.env:empty-environment :operation ',(car expression))))
;; Insert the private keys now
(mapcar (lambda (k) (cl-rm.env:put-private-key cl-rm.env:*environment* k)) ,keys)
(let ((,rest (list ,@(cdr expression))))
(mapcar #'delete ,rest)
(transact-expression (list* ',(car expression) ,rest)
(apply #',(car expression) ,rest))))))
The entry point is the macro transact. The macro does a lot of things in a few lines it:
- Sets up the compilation environment (seen in
(let ((cl-rm.env:*environment*...)))). - Put the private keys into the environment (
mapcar…). - Run the expression to get the result.
- Run delete on the arguments to the outer function
- Form the transaction.
This can best be seen with an example
TEST> (verify-compliance-unit (transact (+ 1 2 3 4 5)))
T
TEST> (macroexpand-1 '(transact (+ 1 2 3 4 5)))
(let ((cl-rm.env:*environment* (cl-rm.env:empty-environment :operation '+)))
(mapcar
(lambda (cl-rm::k)
(cl-rm.env:put-private-key cl-rm.env:*environment* cl-rm::k))
nil)
(let ((#:cdr631 (list 1 2 3 4 5)))
(mapcar #'cl-rm:delete #:cdr631)
(cl-rm::transact-expression (list* '+ #:cdr631) (apply #'+ #:cdr631))))
T
Now let us see in the full gory details what the transact-expression does.
(defun transact-expression (expression result)
(let* ((consumed (cdr expression))
;; just using the car isn't the most elegant
(function (make-instance 'method-resource
:gf (car expression)
:num-args (length consumed)))
(results (list function result))
;; We are filtering out resources that are in the inputs that
;; emit themselves. This isn't full proof as we really should
;; use remove-duplicates, however this has the issue of
;; removing (+ 1 1).... I think I need to implement a better
;; system for function application to better see what
;; arguments it takes
;;
;; A more robust system is to mark what slot I care about and
;; what positions do I need to apply this in, that should
;; work generically
(full-consumed
(mapcar #'obj->resource
(append consumed
(remove-if (lambda (x)
(member x consumed))
(consumed cl-rm.env:*environment*)))))
(full-created
(mapcar #'obj->resource
(append results
(remove-if (lambda (x) (member x results))
(created cl-rm.env:*environment*))))))
(labels ((create-consumed (object)
(make-instance 'instance
:created full-created
:consumed full-consumed
:consumed-p t
;; modeling of tag not online
:tag object
:environment (cl-rm.env:lookup-metadata-table
cl-rm.env:*environment*
object)))
(create-output (object)
(let ((obj (create-consumed object)))
(setf (consumed-p obj) nil)
obj)))
(make-compliance-unit
;; Order is: function, output, created, inputs, consumed
(append (mapcar #'create-output full-created)
(mapcar #'create-consumed full-consumed))))))
This is a lot of code but it’s not too bad. We can see that we make the method-resource we showed before and that goes into results which get fed into fully-created. There is some juggling of the environment to make sure values added into the compilation environment are not duplicated within the results or fully-created. All the arguments (in the example above 1 2 3 4 5) gets added to fully-created as well.
We can see in the create-consumed function (bound by labels), takes the environment at this point and adds the proper metadata-table we discussed before at the given object.
At the very end we make the compliance unit appending together the fully-created and the fully-consumed.
How does it work in practice
With the compiler model out of the way, what does user code look like?
For all these functions, I will provide the entirety of the source
A lot of the usage in practice is through the use of mixins. Mixins are objects that one can include (inherits) from that give you access to certain interfaces or allow methods to be combined with certain properties. In our case, we use it to enhance the functionality of particular methods by doing the following
(defclass mixin-class () ())
(defclass my-cool-class (mixin-class) ())
(defmethod foo :around ((arg1 mixin-class))
(and (call-next-method)
nil))
(defmethod bar :after ((arg1 mixin-class))
(format t "hello"))
(defmethod foo ((arg1 my-cool-class))
t)
(defmethod bar ((arg1 my-cool-class))
1)
TEST> (foo (make-instance 'my-cool-class))
NIL
TEST> (bar (make-instance 'my-cool-class))
hello
1 (1 bit, #x1, #o1, #b1)
Here we have mixin-class and my-cool-class which inherits from it. We can see when we called foo on my-cool-class that it returned nil, this is because the around method for mixin-class went off first which ands the result of it running on my-cool-class and nil, meaning it’s always nil.
For bar the printing of “hello” goes off after it returns 1.
That is to say, even if we overload the method we automatically get the behaviours specified with no effort on the user’s side.
We always use the pattern and in practice, implying that we could potentially change how the class combination works to make it even less boilerplatey.
Ownership
https://github.com/anoma/cl-rm/blob/ad1680d5fcc709da954d0110fd4d5ba13ca0ae57/src/user/ownership.lisp
(in-package :cl-rm.user)
;; Without more scaffolding we can't do much, as we want to sign over
;; numbers for validity
(defclass ownership-mixin ()
((owner :initarg :owner :accessor owner :type ironclad:ed25519-public-key)))
(defmethod cl-rm:delete :after ((object ownership-mixin))
;; We want to instantiate the signing in the env if we have it
(try-signing object))
(-> try-signing (ownership-mixin) t)
(defun try-signing (object)
;; We store the key here for now, not great but w/e
(let* ((env cl-rm.env:*environment*)
(priv (cl-rm.env:lookup-private-key env (owner object))))
(when priv
(~>> env
operation
cl-rm.utils:symbol-to-bytes
(ironclad:sign-message priv)
(cl-rm.env:put-metadata env object :signature)))))
(defmethod holds-on-use :around ((object ownership-mixin) (instance instance))
(and (call-next-method)
(let ((sig (fset:lookup (environment instance) :signature)))
(and sig
(some (lambda (r)
(and (c2mop:subclassp (class-of r) 'method-resource)
(ironclad:verify-signature
(owner object)
(cl-rm.utils:symbol-to-bytes (gf r))
sig)))
(created instance))))))
Ownership is very cute, all we define a structure that just hosts a public key. Meaning that everything owned simply has a public key. When we try to use use/delete an owned object, we end up calling try-signing which looks-up the private key from the environment and puts the signature in the app-data for the given object. The signature is over the method-resource that is being ran, so we require the method-resource to be in the same action to run against.
We only define holds-on-use which simply checks at verification time that we have really signed over the method-resource that is created. The most interesting thing in this is that we call some which tries this against all resources and returns true if any of them are a method resource that we’ve signed over.
Let us look at a brief usage
(defparameter *alice-key* (ironclad:generate-key-pair :ed25519))
(defparameter *bob-key* (ironclad:generate-key-pair :ed25519))
(defparameter *alice-public*
(ironclad:make-public-key :ed25519 :y (ironclad:ed25519-key-y *alice-key*)))
(defclass only-owned (ownership-mixin)
((value :initarg :value :accessor value)))
(defmethod always-true ((object only-owned)) t)
(defmethod holds-on-use ((object only-owned) (instance instance)) t)
(defmethod holds-on-intro ((object only-owned) (instance instance)) t)
(defun alice-1 ()
(make-instance 'only-owned :value 1 :owner *alice-public*))
(defun Properly-signed-away ()
(transact (drop-all (alice-1)) :keys (list *alice-key*)))
(defun improperly-signed-away ()
(transact (drop-all (alice-1)) :keys (list *bob-key*)))
TEST> (verify-compliance-unit (properly-signed-away))
T
TEST> (verify-compliance-unit (improperly-signed-away))
NIL
Unique
https://github.com/anoma/cl-rm/blob/ad1680d5fcc709da954d0110fd4d5ba13ca0ae57/src/user/unique.lisp
An unique object is an object whose creation and consumption is important and is unique from other objects that may have the same fields.
We model it as the following
(defclass unique-mixin ()
((already-made :initarg :already-made
:accessor already-made?
:initform nil)))
(defgeneric use (unique)
(:documentation "Emits the unique object being used into the transaction
I am important to call whenever an operation uses the unique data"))
(defgeneric create (unique)
(:documentation "Emits the unique object being used into the transaction"))
(defgeneric related-use (unique)
(:documentation "I emit extra objects into the transaction space called by `use'")
(:method ((u unique-mixin)) t))
(defgeneric related-create (unique)
(:documentation "I emit extra objects into the transaction space called by `create'")
(:method ((u unique-mixin)) t))
(defmethod use ((object unique-mixin))
(cl-rm.env:emit-consumed object)
(related-use object))
(defmethod create ((object unique-mixin))
(cl-rm.env:emit-created object)
(related-create object))
(defmethod cl-rm:delete :after ((object unique-mixin))
(use object))
(defmethod initialize-instance :after ((instance unique-mixin) &key &allow-other-keys)
;; We should abstract, user code should not care about this!!!
(unless (already-made? instance)
(setf (already-made? instance) t)
(create instance)))
(defmethod copy-instance :after ((object unique-mixin)
&rest initargs &key &allow-other-keys)
(apply #'initialize-instance object initargs))
Here we define out a new API:
- use
- create
- related-use
- related-create
Users are expected to make their own methods for related-create and related-use if they wish for any objects to be created or destroyed with them. This effectively creates a relation between resources/objects.
Besides that, we tie use with delete per the API’s described before, and tie the initialization with creating the instance.
All these get added to the environment as expected.
The most unexpected point of code is the unless in initialize-instance and the copy-instance methods. The first is because I often allocate the same resource from an object over and over so we use the boolean to check if the resource is already made to mask functional creations and transformations, and the copy-instance is because I want to ensure this logic goes off even when copying an object.
Fixed-Supply
Fixed supply is where the strengths and weaknesses of the model both show
(defclass fixed-supply-mixin (unique-mixin)
((supply-quantity :initarg :supply-quantity :accessor quantity :type integer))
(:documentation "I maintain the invariant that things are of a fixed supply"))
(defclass fixed-supply-intent (cl-rm.mixins:pointwise-mixin) ; just for equality
((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"))
(defmethod related-create ((fixed fixed-supply-mixin))
(cl-rm.env:emit-created (make-fixed-supply-intent fixed nil)))
(defmethod related-use ((fixed fixed-supply-mixin))
(cl-rm.env:emit-created (make-fixed-supply-intent fixed t)))
(-> make-fixed-supply-intent (fixed-supply-mixin boolean) fixed-supply-intent)
(defun make-fixed-supply-intent (fixed-supply create)
"Makes a `fixed-supply-intent' on the given instance, the second argument is
for if we should create or consume"
(values (make-instance 'fixed-supply-intent
:quantity (quantity fixed-supply)
:class-assurance (class-name (class-of fixed-supply))
:should-create? create)))
(defmethod always-true ((object fixed-supply-intent)) t)
(defmethod holds-on-intro ((object fixed-supply-intent) (instance instance)) t)
(defmethod holds-on-use ((object fixed-supply-intent) (instance instance))
(some (lambda (finding)
(and (eq (class-name-of finding) (class-assurance object))
(= (quantity finding) (quantity object))))
(if (should-create? object)
(created instance)
(consumed instance))))
(defmethod holds-on-use :around ((object fixed-supply-mixin) (instance instance))
(and (call-next-method)
(fixed-supply-holds object instance t)))
(defmethod holds-on-intro :around ((object fixed-supply-mixin) (instance instance))
(and (call-next-method)
(fixed-supply-holds object instance nil)))
(-> fixed-supply-holds (fixed-supply-mixin instance boolean) boolean)
(defun fixed-supply-holds (object instance using?)
(some (lambda (finding)
(and (eq (class-name-of finding) 'fixed-supply-intent)
(eq (class-assurance finding) (class-name (class-of object)))
(= (quantity finding) (quantity object))
(eq using? (should-create? finding))))
(created instance)))
;;; #############################################################################
;;; API #
;;; #############################################################################
(defmethod split ((fixed fixed-supply-mixin) number)
(when (> (quantity fixed) number)
(use fixed)
(list (copy-instance fixed :supply-quantity number)
(copy-instance fixed :supply-quantity (- (quantity fixed) number)))))
For fixed-supply, we inherit from the unique-mixin, which deals with all the creation logic for us! All we have to include is the quantity we care about. Further we care about a fixed-supply-intent. This is our first intent resource and it cares about the quantity to check against (same field semantics), the class it was created for (remember any class can inherit from fixed-supply, so we need to tie it to a spacebuck for a spacebuck and not an applebuck!), and if the given spacebuck should be created or not.
For this demo all values stored in the fixed-supply-intent are stored in the value, which is an known issue, however some simple code on inheritance can move it to the label, however this is not vital to the model can be changed at the cost of knowing to do it.
All we have to do is define the related-create and related-use which enforces that a fixed-supply-intent is made.
The logic for fixed-supply-intent doesn’t care if it’s created and it’s always true but the logic for holds-on-use is short and describes a simple strategy. It simply looks over all resources and ensures that it can find the same class it intends to create or consume and checks that it’s quantity is the same as it’s. This is in a different actions hence why we stored the original quantity to check against.
Likewise for the fixed-supply-mixin we define holds-on-use and holds-on-intro, which both explicate that the object should be precisely what we are but should be created instead of consumed or vice versa, and has the same quantity etc etc etc.
This code I’d argue is rather readable, as we just check that some resource in the created or consumed has this property.
This has the issue however that we are using some in which we can mount an exploit, can you spot it?
Namely if we create n spacebucks in action 1, and do this for n actions we can satisfy this by simply burning n spacebucks in a single actions, minting many spacebucks.
This is because we don’t check the constraints, rather than setting a metavariable property, we just check that one of the resources satisfy a boolean constraint instead of an integer constraint.
This implies that the model is still too low level, even if the code we create is quite high level.
Spacebucks
Spacebucks with the above is quite trivial with the two above classes.
(in-package :cl-rm.user)
;; Mainly here for example, "tokens" are trivial
(defclass spacebucks (ownership-mixin fixed-supply-mixin) ())
(defmethod always-true ((object spacebucks)) t)
(defmethod holds-on-use ((object spacebucks) (instance instance)) t)
(defmethod holds-on-intro ((object spacebucks) (instance instance)) t)
we can rest entirely on the two above mixins working, and defining out their around methods, meaning both properties are checked like expected.
Ideally we should have an issuer-mixin instead of a fixed-supply-mixin but that is not vital for experimentation and so was not modeled.
Imagining a Logtalk Implementation
We described earlier in the post that our method-resource was insufficient as it was and we saw in the last section that we had a vulnerability because we did not make logical constraints onto the model.
Prolog is a declarative programming language, meaning that it is all about making relations, and being able to solve unspecified equations.
connected(X, Y, Z) :- connected_(X, Y, Z).
connected(X, Y, Z) :- connected_(Y, X, Z).
connected_(bond_street,oxford_circus,central).
connected_(oxford_circus,tottenham_court_road,central).
connected_(bond_street,green_park,jubilee).
connected_(green_park,charing_cross,jubilee).
connected_(green_park,piccadilly_circus,piccadilly).
connected_(piccadilly_circus,leicester_square,piccadilly).
connected_(green_park,oxford_circus,victoria).
connected_(oxford_circus,piccadilly_circus,bakerloo).
connected_(piccadilly_circus,charing_cross,bakerloo).
connected_(tottenham_court_road,leicester_square,northern).
connected_(leicester_square,charing_cross,northern).
reachable(X, Y, Path) :-
reachable_(X, Y, [X], ReversePath),
reverse(ReversePath, Path).
reachable_(X, Y, Seen, [Y | Seen]) :- connected(X, Y, _).
reachable_(X, Y, Seen, Path) :-
connected(X, Z, _),
\+ member(Z, [Y | Seen]),
reachable_(Z, Y, [Z | Seen], Path).
Don’t worry too much about the code above, but notice what happens when I try to call reachable
?- reachable(bond_street, charing_cross, X).
X = [bond_street, oxford_circus, tottenham_court_road, leicester_square, charing_cross] ;
X = [bond_street, oxford_circus, tottenham_court_road, leicester_square, piccadilly_circus, charing_cross] .
- reachable(bond_street, X, [bond_street, oxford_circus, tottenham_court_road, leicester_square, charing_cross]).
X = charing_cross.
it can solve for X! Namely it can give me multiple satisfactory answers, further I can fill in the path (the last argument), and get the destination, meaning we can call this in any order we’d like!
Logtalk is an OO version of prolog that adds in all the normal object systems we all know and love. It is done in such a way that satisfies all the properties that we have in the CL implementation, and thus could be seen as an appropriate candidate for experimentation.
Intent Transactions
In the post we did not mention Intent Transactions, instead we discussed fully applied methods that we worked over. I believe if we want intents that can be properly solved by various entities, then the method-resource above must be able to be:
- partially applied
- able to give constraints
- be able to shield various constraints
Property 1. allows us to take methods that we have an instead of giving concrete arguments like (5 spacebucks), we can instead replace it with a meta-variable that can be filled in at a later time. For a solver, they can impose extra constraints on this meta variable, such as “X must come from my pool of liquidity”.
Property 2. allows us to combine the partially applied intent-operation with others to constraint the space of possible solutions. So a constraint may be that this method has the constraint that it takes a spacebuck and it must have quantity larger than 3, then this is a constraint on it’s acceptance criteria. Meaning that we leak all the necessary information to be able to solve it and compose a transaction that can pass the resource-logic
Property 3. allows us to hide information from solvers, maybe we would only like to give a fraction of the constraints such that we hide information we don’t want to leak.
Further since we can fully run the logic, we can now get the logical output the user expects meaning we can create the resources that we initially wanted to and ensure that it happens in a relational matter.
Vulnerability
Before we saw the vulnerability of using some I believe we need further research here, but if we do it correctly, we should describe the abstraction ontop of resource logic’s as declarative as possible, I’d argue rather than just checking individual resource logics, we should create a framework that sorta runs all resource logics, and have them pose constraints over the solution space and make sure everything passes there. This would allow the right pattern of constraining the number of fixed-supply to be an integer constraint instead of a pure boolean one which causes the issue.
The Meta Language Requirements
With the model explained, what properties are required to make this system work?
- We require the resource machine to be modeled in the given language we are working in.
- Otherwise we can not have tight control of compilation making the layered approach that allows efficiency to not work.
- We require multiple inheritance or some kind of mixin mechanism
space-bukcsinherited from two separate mixins.
- We require aspect oriented programming
- These are the
:afterand:aroundthat all our mixins took advantage of.
- These are the
- We require generic data traversal of our data types
- These can be seen in us mapping objects to resources and back again.
- We need to be able to hook into object allocation life cycles
- See the method initialize-instance in the code above and the delete API.
- We need to be able to reference a meta environment that compilation is happening inside of
- This is shown in the environmental API
- For Intents we need to be able lay out declarative constraints
- See the section on Prolog/Logtalk.
These are not all the requirements, just the requirements that we have found in this prototyping and musing about what this could look like in Logtalk.
Conclusion
Overall the Object Oriented model seems to fit well into how the RM works. We have seen logic which is somewhat intuitive but still not high level enough yet for real application development. Further exploration is required in logical constraints and the right user level interfaces that we should go with. Once these are found and agreed upon, we can make a real demo implementation for the first version of Anoma Level inside of Elixir.