Here are my preliminary notes. Note that Iβm a non-expert when it comes to crypto stuff, so things that someone familiar with the field might take for granted, I cannot. Iβm mostly coming at this from a mathematical perspective. If I wanted to formalize a resource machine as a concrete mathematical structure, what would that look like? To that end, Iβm fixating mostly on ambiguities and things that I canβt make sense of, and giving some recommendations for clearer exposition along the way. I also just finished reading it, so my understanding of what a resource machine is supposed to be is undeveloped. Some of these might be obvious or pointless to others, but I hope this is helpful anyway.

### Page 1:

We say a field to refer to a component of some composite structure

You never define what a composite structure is. It seems to be a record with named fields.

We say a field to refer to a component of some composite structure π

Youβre not consistent about using the word βfieldβ instead of βcomponentβ, and I donβt see a good reason to use this terminology. Why not just always say βcomponentβ? You could then say βcomputable componentβ instead of βcomputed fieldβ, etc.

A computed field of π is a value that is not a field of π but that can be derived

solely from the composite structure π fields.

I think what this is trying to say is that the computed fields are trivially derivable from other fields. This sentence isnβt correct as later computed fields are computed using hash functions being applied to other fields, so, not βsolelyβ; you also need the hash function. If a hash is always involved, maybe you should move the mention of computed fields until after hashes are mentioned. You can then define computed fields as hashes of other fields. Also ensure to mention that computed fields can be created from other computed fields (e.g. π
.Ξ), as the default interpretation of just βfieldβ on its own would be the non-computed fields.

The grammar of this sentence suggests that βfieldsβ is a verb, an action that S is performing, which is obviously wrong. So this sentence should be rephrased even if you donβt take my previous advice.

Let π» be a class of hash function

Where does H live? Is it part of the data within the machine itself, or is this just defining a type of hash function?

such that the output of any function in π» forms a finite field.

Is the range a field, or is the image a field? For example, can I have the outputs be, say, graphs, and then define a field over the finite set of graphs defined by the image of H? Are there restrictions on the input?

Iβm also not sure about having π» at all. Itβs never really used. Itβs mentioned as containing the hash functions in the βResource Computable Fieldsβ section, and thatβs it. I donβt see why we need a symbol when all it refers to is the hash functions listed in that section, and we donβt ever need to talk about the set of those functions.

and the corresponding to β finite field is denoted as πΉβπ₯

Rephrase to βand the finite field corresponding to β is denoted πΉβπ₯β.

We use π₯π (βπ₯-setβ) to refer to a set of objects of the same type as π₯.

Is x a type? Or is x a component, like in the previous paragraph? Taken literally, this says that x should be an element of some type, and βxsβ is referring to that type itself, but thatβs awful. It would imply that, for example, β25sβ means the natural numbers since 25 is a natural number.

I also donβt think this line is that helpful, as this is just a naming convention, not a notation that needs to be explained. Where it appears, βxsβ is just a name, itβs declared to be a set, and it doesnβt need further explanation, IMO. I spent too long trying to figure out what this line was saying when what itβs saying is already obvious from the context where itβs used.

### Page 2:

πππππ : πΉ_πππππ

Many of the "F"s in the resource definition should be in blackboard bold (i.e. using \mathbb) but arenβt.

Resource Computable Fields

Are these hash functions the same across different resources? Or are they global; part of the definition of the resource machine? Or are they universal; the same across different resource machines? This is essentially the same question as before, where does βHβ live?

Address π.ππππ = ππ = β_ππ(π)

Shouldnβt it be βAddress π.ππππ = r.ππ = β_ππ(π)β? Also, why have separate bullets? Canβt one just say cm is also called addr since itβs used as an address? Also, the βr.ππππβ notation is never used, so thus bullet can be dropped entirely.

When a resource is created, its commitment is added to an append-only global

commitment tree.

What is an βappend-only global commitment treeβ? Is it a Merkle tree? Where does it live? Is it part of the resource machine, or is it an external thing the machine has access to?

Delta π
.Ξ = βΞ(π
.ππππ, π
.π)

Why is βRβ capitalized here when itβs lowercase on the other bullets?

Proving system

Where do proving systems live? Are they part of the data within the resource machine, so every resource logic uses the same proving system? Or does every resource logic have its own proving system?

Remark 1. The hash function used to derive Ξ must have additive homomorphic properties [β¦]

The algebra should be spelled out explicitly through equations. Something like

- βΞ(K, q1) + βΞ(K, q2) = βΞ(K, q1 + q2)

It should also be made clear what itβs a homomorphism of. If ββΞ(K, 0) = 0β doesnβt hold then itβs not a monoid homomorphism.

when deltas of two resources of different kinds are added, their quantities stay independent of each other

I donβt know how to interpret βtheir quantities stay independent of each otherβ, itβs not clear what that could mean.

ππππππ¦(π£π, π₯, π) : ππ.ππππππ¦ππππΎππ¦ Γ ππ.πΌππ π‘ππππ β F_π΅"

Should this have βππ.πππππβ as one of its input types? Also, what is π΅? Thatβs not mentioned before this. Did you mean F_π, for the boolean field?

A proof record carries the components required to verify a proof.

This is the same data thatβs taken as input for Verify, but in a different order. Thatβs quite messy. Why not make Verify : ππππππ
πππππ β F_b? That way, you donβt need to permute a proof record to verify it.

### Page 3:

A partial transaction is a mutable composite structure

What does βmutableβ mean? I know what it means in the context of programming, but I think this is trying to handwave something that really needs to be described explicitly. Iβll write about this more at the end of my note, but what actually is a resource machine, and how does its data evolve during execution? The answer to this question is given in disparate pieces implicitly throughout the paper but is never described explicitly. βmutabilityβ canβt be made sense of without a more explicit description of the architecture. Where are the partial transactions stored so that they can be mutated, and what update function is being applied to perform the mutation? What does the global state transition look like; specifically where/when does it call the mutation update function? I suppose all that doesnβt need to be explained at this part of the paper, but it should be explained somewhere.

A partial transaction is a composite structure π π π = [β¦]

Resources are defined in terms of a large product but partial transactions are not and a name for the type of partial transactions is never given. This is an inconsistency that should be easy to fix.

πππ : {ππ : Fππ}

This notation is very confusing and suggests that βanβ is an element of the set βFanβ, so every βanβ is part of a different set indexed by itself. Very strange. I think this is trying to say that βansβ is a set of "Fan"s, and that any particular element of this set is called βanβ. Same thing with βπππ : {ππ : Fππ}β and βππ π : {ππ : Fππ }β. In these lines, βanβ, βππβ, and βnfβ donβt seem to actually refer to a specific element, but are just part of the naming schemes for example elements, so I think their mention can be dropped entirely without causing confusion. It may be helpful to explain where the names come from. βcmβ standing for βcommitmentβ is obvious, but where does βanβ come from?

πππ : {ππ : Fππ} is a set of roots (from different epochs) of the global resource commitment tree.

Is the βglobal resource commitment treeβ the same as the βappend-only global

commitment treeβ mentioned earlier? It would probably be a good idea to make symbols for all the global data structures and use those symbols when referencing them.

Ξππ‘π₯ : πΉΞ is computed from Ξ of input and output resources (signed addition).

Isnβt the Ξ computed using hΞ? Where does signed addition come in? And when and where are these requirements enforced? This is another place where the architecture is hinted at without being described explicitly. If Ξππ‘π₯ is a computed Ξ, how is that? If πΉΞ is just a field, then the partial transaction canβt seemingly know where it came from. Ξππ‘π₯ is just a field element, and it being some kind of difference must be enforced by something outside the partial transaction, and itβs unclear whatβs doing that and how.

Alternatively, is this actually a computed field? If so, then it should be separated from the other fields, as it looks like data of the ptx that has to be checked for correctness rather than something computed from the ptx.

is a post-ordering execution function

What does βpost-orderingβ mean?

q = 5 [β¦] π = π_πππ₯ = |πΉ_π| β 1

F is not in blackboard bold. Also, where does this field come from? It doesnβt look like itβs used by any hash function. And why does πΉ_5 have 6 elements, according to this?

Each partial transaction contains a set of resources to be consumed and a set of resources to be created.

This is not true according to the definition just given. Is this referring to the cms and nfs? Those are field elements, not resources. If I understand this properly, they are essentially names of resources that can be looked up to get the actual resources. However the resources themselves are not part of the partial transaction.

For each resource consumed or created in a partial transaction, it is required to provide a proof that the logic of the resource evaluates to 1 given the partial transaction parameters

The βresource logicβ terminology is really confusing. It should probably be renamed to βresource constraintβ, or something like that. It doesnβt make much sense for a logic to evaluate to 1.

Ξ proof (balance proof) [β¦]

It would be good to write this out explicitly in more mathematical terms. Itβs not clear what Ξ composition is, how they are extracted from resources, or how the check actually occurs. Is composition just a linear combination? The way itβs written, it sounds like they are separate things (one is the value, while composition is something else thatβs not specified).

RM compliance proof [β¦]

Being explicit in more mathematical terms about what this looks like would be good. Thereβs a lot of moving parts here, and a detailed list of descriptions is necessary, I think. Also, what is βRMβ? Is this supposed to be βARMβ, or whatever other acronym we settle on?

It also requires explicit check of the presence of all other required proofs.

Where do the other required proofs come from? Are they part of the data of the resource machine? Are they the same thing as the βmandatory inputs and checksβ mentioned later in the Resource Logic section?

### Page 4:

ππ₯ππππ‘π₯ = πΉ (ππ₯ππ1, ππ₯ππ2) [β¦] Ξ¦ππ‘π₯ = πΊ(Ξ¦1, Ξ¦2)

Itβs fine to have F and G as parameters for composition, but it would be good to have some guidance for what sort of things they would be in practice.

F is used elsewhere to represent fields. While I donβt think this will cause confusion, it may be wise to change these variable names so thereβs no clash.

Remark 4. For parameters composed with the disjoint union operator, it has to be checked that those sets didnβt have any elements in common, otherwise the partial transactions cannot be composed.

Why? Disjoint unions generally label the elements of the two sets so there isnβt an overlap; why canβt that be done here, and why does that not apply to πππ ? Why do the disjoint unions need to be disjoint to begin with? Thereβs a lot of unexplained intuition packed into this remark.

Executable. The system used to represent and interpret executables

Are these related to earlier EXECs in the π π πs? If so, the earlier declaration that πΈππΈπΆ = π π π β π π π is wrong, as whatβs being described in this new section is a first-order representation that can be interpreted as a function. Instead, there should be something like a function of type βeval : EXEC Γ PTX β PTXβ, and EXEC should actually be defined to be a kind of Nockma program. If Iβm wrong, then a clarification that weβre talking about different executables should be made.

π
πΈπ΄π·_ππ ππ
π΄πΊπΈ(ππππππ π : Fππ)

What does this actually return? An integer? An element of some other field? An actual resource? If that last one, is there a read function for nfs? If not, how does one get the resource associated with the hash generated by h_nf? Thatβs needed for the private input resources of a Resource Logic.

If the value is not found, the operation should return an error.

What does this mean? Again, the resource machine is being described implicitly, in parts, but the whole is not clear.

π
πΈπππ π
πΆπΈπ_π΅π _πΌπ π·πΈπ(πππππ₯_π π’πππ‘πππ)

What are index functions and where do they come from? Whatβs an example of an index function? The only example of an index function mentioned in the paper appears on page 5, where itβs stated that βan index lookup uses the value stored at the address as an index functionβ. So, is an index function a function at all, or are you using a lookup table that contains addresses and calling that a function?

The executable might update partial transaction data fields,

What is an update? Again, this is implicitly describing the machine architecture without describing it explicitly. How are updates done? Presumably, this relates to the earlier comment on mutability. This is really a global architecture question. This section describes an update function, but where it lives (itβs part of the machine, right?) and how/when itβs used is less clear.

ππππ’ππ‘ [β¦] ππππππ‘

Where are these variables stored? Are they part of the machine?

If ππππ’ππ‘ > ππππππ‘, the execution halts with an error indicating the gas limit was exceeded.

What are errors? What does it mean to halt? Error handling would be part of the machine definition, but, again, this is mentioned offhand without ever being described explicitly.

Recursive calls first increment the counter ππππ’ππ‘, then recurse

Are executables even capable of recursion? It doesnβt seem like it, based on the Nockma description later on. If a pattern reduction step is executed, but itβs not recursion, just a step of evaluation, does that still increase gcount?

### Page 5:

6.2. Resource Logic. A resource logic is a predicate [β¦]

A Resource Logic *represents* a predicate, but itβs not literally a predicate (that is, a function from a set onto the booleans). We can extract a predicate from a resource logic, but it clearly has more structure.

The evaluation context of a Resource logic is a partial transaction.

This is contradicted by the later

- input resources corresponding to the elements of ππ π
- output resource corresponding to the elements of πππ

The partial transactions do not contain the resources themselves, only their names, so clearly the context must be more than just the partial transactions. Presumably, the context also includes the βglobal content-addressed storageβ and βglobal resource nullifier setβ. These might be made accessible by functions in the program language itself, but in section 6.1, βπ
πΈπ΄π·_ππππ
π΄πΊπΈβ is described as an IO function, and the beginning of 6.2 states that resource logics do not require IO, so I donβt know.

Resource logics are customizable on both implementation of a resource machine and resource logic creation level. A concrete implementation of a resource machine can add more mandatory inputs and checks

This should really be spelled out explicitly by describing how information flows between/through the resource machine and the logic.

Hereβs my best guess for how this should work: I think that a resource logic is a Nockma program with access to variables representing the cms, nfs, and actual resource data associated with them from the relevant partial transaction. A PS.Proof is a ZKP of the trace of the program attesting to it outputting βtrueβ. And the resource machine has, as part of its data, a Nockma program thatβs run prior to the resource logic program, and the ZKP should also verify its trace ends in βtrueβ as well.

Thatβs my best guess for how this is supposed to work, but Iβm not confident at all. Whatever the case is, it should be stated explicitly.

Verifiability. It must be possible to produce and verify a proof of type π π.π ππππ that given a certain set of inputs the resource logic output is πππ’π

βTrueβ is not a possible output according to the Nockma specification given later on. Should this be β1β, representing true?

ππ π β ππ π ππ‘π₯

Why canβt the resource logic mention all the nullifiers or commitments? That is to say, why are these proper subsets instead of improper subsets?

custom inputs

How are custom inputs stored and read?

for each output resource, check that the corresponding ππ value is derived according to the rules specified by the resource machine from its fields

What are the fields of a resource machine? Thatβs never described. Or is this the cm resource fields? If the latter, do fields need to be mentioned here?

### Page 6:

Pattern

An explicit syntax for patterns would be helpful. Itβs clear that the syntax for patterns is different for the syntax of nouns, and some patterns donβt have evaluation rules (for example, β?[a b c]β) and it never says what to do in such a case.

finite field πΉπ of order π

This contradicts the previous notation where non-blackboard bold F represents fields that are outputs of hash functions. I would recommend making this F, and all subsequent Fs in this section, blackboard bold.

division operation (floor division)

What happens when dividing by 0?

addition operation ππ Γ ππ β ππ Γ πΉ2

F should be blackboard bold. Same for remaining operations mentioning F2.

the conversion function would return a flag (of type πΉ2)

F should be blackboard bold.

### Examples section

The examples provided are generally understandable, particularly in their depiction of transactions. However, they fall short in offering deeper insights beyond this basic case. It mentions green arrows indicating a state change. Whatβs state is being changed? The resource machineβs? Where is this state being stored so that it can be changed? Presumably, there should be global something-or-others involved, but they go unmentioned. The composition is also unclear. They are just handwaved away with unspecified Fs and Gs, leading to no additional insight. Itβs still unclear what the execs are, for instance, since none are described at all. None of the examples describe specific resource logics, meaning they fail to give examples of things like custom inputs which are still unclear.

### Discussion: What even is a resource machine?

Nowhere in the paper is a resource machine actually defined. Frequently, βglobalβ data structures are mentioned, but itβs never made clear if they are part of the state of the machine or are some external data that the machine can read from. Because of this, whatβs in it is ambiguous. Hereβs a reasonable interpretation:

A resource machine contains the following data;

- A finite set of hash functions, with at least the specific βππ, βππ , βππππ, and βΞ.
- A Merkle tree for commitments
- A table with Fcm entries containing resources
- A table with Fnf entries containing resources
- An integer gas counter
- A set of partial transactions
- A nockma program representing mandatory constraints

such that, at each step, it takes an input from an external clock, and then executes each of its partial transactions. This step is the least clear. There should be some state transition function of some concrete form that does this. It seems like most of the paper is trying to describe the details of this, but the connective tissue that ties this all together isnβt really there. What Iβd like to know is, given a collection of resources and a machine state, how do we get to the next machine state? A timeline describing the order in which every transformation to the state is done would be helpful.

I suspect that some of the things in the previous bullet list arenβt part of the machine, but external things the machine can read from (and I may have described some of these incorrectly), but this hopefully demonstrates ambiguity in the current paper. A more clearly articulated architecture described in terms of an explicit data structure would be extremely helpful.