ART Report: Resource Machine

Protocol Design
5

Thanks for the reviews so far (particularly @AHart - this is fantastic feedback). A few comments from my end (cc @vveiln):

Execution flow

As @mariari mentions, I think we can remove EXEC and stipulate that the Nockma code must simply return a full partial transaction structure - and all we need to define is the verification function (no need to define mutation functions) over PTX.

In that case, we might also want to clarify execution flow. Perhaps we can have a parameter which is passed to the Nockma code - something like:

data ExecTime = PreOrdering | PostOrdering

data ExecInfo = ExecInfo {
  execTime :: ExecTime,
  execWho :: ExternalIdentity
}

In both pre-ordering and post-ordering execution, the Nockma code must return a partial transaction, but the partial transaction returned in pre-ordering execution need not be balanced - this is what the solver would then examine in an attempt to solve (and compose the involved partial transactions, then forward their composition).

The question naturally emerges of whether and how to compose the Nockma code segments of two different partial transactions (or whatever we call the message that contains the Nockma code which returns a partial transaction). For now, let’s not worry about this, and say that the naive solver simply takes partial transaction codes A and B, calculates A, calculates B, and if they can be matched (and balanced) as C returns new Nockma code that simply returns C. In other words, we can worry about hybrid post-ordering matching later.

One problem with passing parameters to the Nockma code like this is that the parameter values aren’t verifiable ex post, so they cannot be checked by resource logics. We might also want to have “sentinel resources” which contain these values if we want resource logics to be able to check them.

Distributed partial evaluation

Relatedly, I think it may be helpful to visualize and articulate how this resource machine, when run in a distributed network, implements what I think can be understood as a form of distributed partial evaluation.

  • resources <> memory states
  • resource kinds <> memory cells
  • partial transactions <> evaluation states

For example (diagram could be greatly expanded), understanding #A, #B, #D, and #E as kinds of resources previously created, #C and #F as kinds of ephemeral resources, and res as some result, the following three partial transactions perform a distributed reduce operation:

Untitled-2023-11-15-1703
Untitled-2023-11-15-1703809×353 17.5 KB

Further input here from the PLT folks (cc @jonathan) would probably be helpful, I’m sure I’m butchering the language, but I think the analogy holds, and it’s worth making explicit.

Resource machine

I agree with @AHart that it would be helpful to more explicitly define a resource machine. In this case, the machine is in fact deterministic and need only process one transaction at a time, executing the Nockma code, validating the returned partial transaction, and either applying the updates (should the partial transaction be valid and balanced) or terminating without any changes (should the Nockma code run out of gas or the partial transaction be either invalid or unbalanced). Anything about sharding should be out of scope, though - that is a detail (feature) of Typhon’s execution engine, which preserves serializability - meaning that we need not care here.

Might have more thoughts tomorrow.

1 Like