[Proposal] Scope refinement for resource machine report v2

[cwgoes]

The purpose of this topic is to collectively agree on the scope for v2 of the resource machine report, most likely coauthored by @vveiln and myself (a wee bit).

Most ideas here are sourced from this thread - I suggest that we pick the most relevant ones under a few criteria:

1. Converging the interfaces to what we expect to be the final shape as fast as possible, so that we can aim to provide application API stability later this year.
2. Clarifying calling conventions and all points relevant to developer UX.
3. Working out & clarifying real examples to aid in both (1) and (2).

Current proposed scope (as an extension to what’s already in v1):

• Balancing signature folding proofs (see here)
• Distributed partial evaluation analogy (see here), times of execution, and details on how transaction candidates may be combined pre-ordering.
• Support for non-linear resources, and example usage as oracle data (e.g. timestamp).
• Information flow control for transactions / transaction candidates, and related details on upgrading / downgrading proofs, information revelation, etc.
• Clarify all calling conventions.
• Additional examples of:
  • Non-linear resources
  • Information flow control & visibility to different parties
  • Account abstraction

Folks who should definitely read over this / give input:

• @mariari & @ray from the developer UX perspective
• @isheff from the Typhon perspective - when / how do we want to integrate controllers here?
• @paulcadman and Juvix folks from the Juvix perspective - are there parts of the API which you would like to be clarified or changed?

[cwgoes]

Notes from discussion:

Examples to cover:

• Counter (w/unique instantiation / built-in resources)
• Token w/account abstraction

Improvements to structure and clarity:

• More consistent & intentional w.r.t. type-theory-like descriptions
• Clarify abstractions & interfaces for transaction candidates, storage, and related topics (e.g. Merkle trees, checks done outside of circuits)
• Add tables to explain symbols used in the report

[cwgoes]

Further exposition on some topics here:

Non-linear resources

Non-linear resources are treated exactly the same as linear resources, except that we allow them to be consumed (read) an infinite number of times. We need to think through exactly how to do this - I can see two options, not yet sure which is better:

• reveal the nullifier, but ignore conflicts
• don’t reveal the nullifier at all, and prevent it from being revealed

The resource logic should receive a parameter indicating whether a consumed/created resource is linear or non-linear, and be able to accept/reject based on this information.

Times of execution and types

• Let Transaction be the type of a fully determined state change (as currently described in the RMv1 report).
• Let TransactionCandidate and TransactionPayload be the data structures as defined by Typhon here.
• Let TransactionFunction be the Nockma executable, which - when fully applied post-ordering - must return a Transaction. This is roughly synonymous with TransactionCandidate as defined in the RMv1 report, but I realized that we had a name conflict between RM & Typhon here, and I think TransactionFunction is clearer anyways.
• In usage with the RM, Typhon’s TransactionPayload type will be a synonym for TransactionFunction.

Pre-ordering execution is defined as execution of a TransactionFunction before the ordering of this transaction with respect to all other transactions has been finalized. In pre-ordering execution, a TransactionFunction must return another TransactionFunction (partial application).

Post-ordering execution is defined as execution of a TransactionFunction after the ordering of this transaction with respect to all other transactions has been finalized. In post-ordering execution, a TransactionFunction must return a Transaction.

We should also clarify matters with respect to the executor function type as defined here.

[cwgoes]

Counter example

The counter example consists of:

• a special unique_id resource which:
  • is tied to a specific controller
  • is initialized by that controller to 0
  • can be consumed and created iff. it is incremented by 1 and that controller signs
• a resource logic for the counter, which should:
  • allow the counter to be consumed and created iff. the new counter is equal to the old counter + 1
  • allow the counter to be initialized (created from scratch) with a label l iff. l is equal to the value of the current unique_id resource
• example transactions to initialize and update the counter

Token & account abstraction example

The account abstraction example consists of:

• a token, as in previous examples, but where the value field contains a denomination (of another resource) instead of a public key, and where the token resource logic allows tokens to be transferred iff. a resource of the specified denomination is created in the transaction with a message authorizing the transfer (whatever would have previously been signed over by the public key)
• a message-authorization resource logic (referenced as the denomination in the above) which allows messages to be created iff. an account resource is consumed/created in the transaction and if the public key in the account resource value signs over the message
• an account resource logic which stores a public key in the value field, and allows the public key to be changed in a transaction
• example transactions to:
  • send the token
  • update the account key

[vveiln]

1. Do we want to also have resources that are consumable n times, where 1 <n < \infty?
2. Why can’t we/don’t we want to create non-linear resources on the application level, when the low-level resource is linear but it is re-created again and again so for the user it is non-linear?

[cwgoes]

@vveiln

• Do we want to also have resources that are consumable nnn times, where 1 <n < \infty1<n<∞1 <n < \infty?

I don’t think we need to model those separately with nullifiers - for that use-case, a resource can allow itself to be consumed and a new version created with some counter decremented, where once the counter reaches zero the resource can no longer be consumed. We could choose to model this with nullifiers but it would result in information leakage (since the same nullifier would be revealed multiple times), so I think that’s probably undesirable.

@vveiln

Why can’t we/don’t we want to create non-linear resources on the application level, when the low-level resource is linear but it is re-created again and again so for the user it is non-linear?

This is also possible, but there are two strong reasons to allow native non-linear resources I think:

• efficiency (much more efficient for ~ read-only data)
• conflict avoidance (application-level non-linear resource reads in different txs would still conflict with each other, at least if they were done in a shielded fashion)

[cwgoes]

Editorial note - I was thinking a bit this morning and realized that we should try to cover some additional topics which probably fit best in this report right now. I’ll summarize each topic in a separate post. First: applications!

Applications

Prose definition

Applications consist of related resource logics, which define the kinds of resource which constitute the application’s state, and transaction functions, which define the actions users can take to interact with the application. The abstraction of an application is virtual - applications are not deployed or tracked in any sort of global registry - rather, they are content-addressed by the specific logics involved. An application can be said to exist by virtue of the existence of resources referencing these logics, and if these resources are completely consumed it no longer exists (except in history). Applications are also composable, in that the delineation of which resource logics constitute one application versus another is a choice made by the user, and that state transitions for multiple applications can be combined (atomically, if desired).

Formal definition

An application logic is defined as a set of resource logics:

ApplicationLogic := Set(ResourceLogic)

Application logics may be composed simply by taking the union of the logic sets:

compose(al1: ApplicationLogic, al2: ApplicationLogic) = al1 \cup al2

An application interface is defined as a set of transaction functions:

ApplicationInterface := Set(TransactionFunction)

Application interfaces may be composed in the default manner simply by taking the union:

compose(ai1: ApplicationInterface, ai2: ApplicationInterface) = ai1 \cup ai2

An application is defined as the conjunction of an application logic and an application interface:

Application := (ApplicationLogic, ApplicationInterface)

In order to be a valid application, all transaction functions in the application interface must refer only to resource logics in the application logic.

valid(a : Application) = scopeCheck(a.interface, a.logic)

Applications may be composed in the default manner simply by composing their components:

compose (a1 : Application) (a2 : Application) = \\ (compose(a1.logic, a2.logic), compose(a1.interface, a2.interface))

Application composition may also open up new, non-trivial interface possibilities on a per-instance basis.

Report integration

All of the examples we describe should instantiate this Application type (often trivially, e.g. with only one resource logic and only one transaction function), and we should describe some example compositions.

[cwgoes]

Editorial note - this topic will be covered in more detail in the controllers report, but I think it’s worth giving a basic overview here of what the application concerns will look like, and the interfaces / constraints here should match up with what the controllers report specifies.

Distributed state synchronization

The basic goal of distributed state synchronization is to allow application state (resources) to be distributed among various independent domains, each of which has their own security model and local ordering, and all of which may execute in parallel, while preserving a single global state namespace, such that resources may (when permitted by their logics) move freely across domains, and while preserving fault isolation, such that faults on one of the domains do not violate any correctness or liveness properties of state living elsewhere.

Recall the description of storage, in particular the commitment tree and nullifier set. Suppose that we have a (possibly infinite) number n of domains, where domain n is identified as D_n.

The basic idea of distributed state synchronization is to:

• Partition the commitment tree into a set of sub-trees, where each sub-tree T_n is associated with exactly one domain D_n, and the overall commitment tree root is a second-order Merkle tree where the leaves are the roots of T_n.
• Fix a domain D_n in each resource such that the resource can only be consumed on D_n. A reference to D_n can be stored in the resource value, and this can be enforced by the resource logic (checking some kind of attestation from D_n). This means, in particular, that each resource can only be nullified on one domain, which is necessary to preserve linearity in a concurrent environment.
• Periodically synchronize sub-trees - for each sub-tree T_n, after some updates (the result of executing transactions), the latest root for T_n is sent by D_n to other interested domains, and they update their commitment tree to reflect it. To preserve fault isolation, this synchronization must come attached with a proof sufficient to prove to the receiving domain that these updates are correct (in the typical resource machine sense).

Resources can then be transferred from one domain to another - say D_a to D_b - simply by:

• Submitting a transaction to D_a which consumes the resource on D_a and creates an identical one assigned to D_b, the commitment for which is now in T_a.
• Wait for T_a to be sent over to D_b via the synchronization process.
• The new resource can now be consumed on D_b.

This system provides several important affordances to applications:

• Applications can support multi-domain usage, interactions, and state transfer without any additional programming required.
• The state synchronization system, with the appropriate sorts of proofs (e.g. zero-knowledge), can preserve full programmable disclosure, such that a third-party observer knows nothing about what state is being transferred between domains apart from what is explicitly disclosed to them.

[cwgoes]

Editorial note - I think adding one more example application which showcases a few related resource logics, application-host interaction, and the separation of concerns induced by this application programming model will be helpful - this is the best minimal example I thought of which covers these concepts.

Example application: proof-of-stake

The basic aim of proof-of-stake - popularized in the “Slasher” blog post - is to assign voting power in a BFT consensus algorithm on the basis of “stake” - units of a particular token (typically native to the consensus domain in question) which are locked up for a certain duration of time, and often associated with specific validators (whose voting power in consensus is proportional to the amount of stake which has been associated - “delegated” - to them). The lock-up is necessary to enable “slashing” - punishment of validators (and often their delegators) for attributable misbehaviour by burning part or all of the tokens locked up, if attributable misbehaviour is discovered during the lock-up period (often called the “unbonding period”).

Here we will describe how to implement a very simple proof-of-stake application using the resource machine. This version of proof-of-stake is missing many features real proof-of-stake systems might want, such as rewards and redelegation, which we omit for the sake of simplicity and conceptual clarity.

Application logic

We assume the existence of a proof-of-stake token T and an unbonding period U.

The application logic consists of four resource logics: pool, bond, withdrawal, and infraction.

• The pool P exists only to own T.
• A bond B has an amount B_{amount}, a validator B_{validator}, and an owner B_{owner}.
  • A bond can be created by transferring B_{amount} units of T to the pool P.
• A withdrawal W has an amount W_{amount}, a validator W_{validator}, an owner W_{owner}, and an unlock timestamp W_{unlock}.
  • A withdrawal can be created by consuming a bond with the same amount, owner, and validator. The unlock timestamp for the withdrawal must be set to now + U.
  • A withdrawal can be consumed after W_{unlock}, transferring A = W_{amount} * \prod_{i \in I, i_{validator} = W_{validator}, i_{timestamp} \le W_{unlock}}(1 - I_{rate}) units of T from P to W_{owner}.
• An infraction I has a validator I_{validator}, a timestamp I_{timestamp}, and a slash rate I_{rate}.
  • An infraction can be created by providing proof that the validator I_{validator} has committed some misbehaviour at I_{timestamp}. For simplicity, we define misbehaviour as only two signatures over distinct blocks at the same height.
  • Infractions can never be consumed (they are non-linear, read-only resources).

Application interface

The application interface consists of five transaction functions:

• The delegate transaction function simply creates a new bond.
• The undelegate transaction function consumes a bond and creates a withdrawal.
• The withdraw transaction function consumes a withdrawal (returning T).
• The slash transaction function submits proof of misbehaviour to create an infraction.
• The calculateVotingPower transaction function iterates over all bonds to compute the current voting power which should be assigned to each validator. This function will typically be used by the host consensus domain to assign voting power in the BFT algorithm.

[vveiln]

I’m gonna go through each topic separately to dedicate more brain power to each, here are my questions about the applications:

1. What is a transaction function?

@cwgoes

if these resources are completely consumed it no longer exists

Doesn’t exist as in “currently the application is not being used” or doesn’t exist as in “dead forever” (and if we want the same functionality again, it technically is a different application)? Because in the first case it exists virtually, and in the second it doesn’t exist in any sense. So does complete consumption of the resources on the low level also “destroys” the application on the virtual level? Asking from the perspective where some applications do not maintain a state and do not require any resources existing, e.g. an intent application never has unconsumed resources, so it kinda never exists

@cwgoes

the delineation of which resource logics constitute one application versus another is a choice made by the user

So composed applications exist on a somewhat different level of virtuality than atomic applications, i.e. atomic applications have an explicit resource logic that defines them and composed application resource logic is implicitly composed from multiple resource logics? Even though there is a formal definition of a composed application logic, if the choice is made by the user I assume the composition will not be explicit (e.g., there will be no explicit interface for every composed application but can be for a composed application someone decides to build an explicit interface for)

@cwgoes

An application logic is defined as a set of resource logics

Do we want some kind of structure here? How do we ensure that all of them are satisfied? Or how do we pick the ones to satisfy, if we don’t necessarily want all of them to be satisfied?

4.1

@cwgoes

Application logics may be composed simply by taking the union of the logic sets

If a composed application logic is the union, it either implies that we assume the satisfaction of all resource logics at once (which would make sense, but just checking if we do) or we introduce a lot more variability for composed application logic instances, which sounds like a mess without specified logic enforcement rules

[cwgoes]

@vveiln

• What is a transaction function?

A transaction function is my proposed new name for what we previously called (in the RMv1 report) transaction candidate. Typhon uses the name transaction candidate already for a different data structure, and I think transaction function is clearer anyways - a transaction function is simply a function (for now, in Nockma) which returns a transaction.

@vveiln

Doesn’t exist as in “currently the application is not being used” or doesn’t exist as in “dead forever” (and if we want the same functionality again, it technically is a different application)? Because in the first case it exists virtually, and in the second it doesn’t exist in any sense. So does complete consumption of the resources on the low level also “destroys” the application on the virtual level? Asking from the perspective where some applications do not maintain a state and do not require any resources existing, e.g. an intent application never has unconsumed resources, so it kinda never exists

The former - in this model, applications have no identity other than their resource logics and transaction functions. I think you are right - better to say that applications are virtual, and they always exist (but only virtually).

@vveiln

So composed applications exist on a somewhat different level of virtuality than atomic applications, i.e. atomic applications have an explicit resource logic that defines them and composed application resource logic is implicitly composed from multiple resource logics? Even though there is a formal definition of a composed application logic, if the choice is made by the user I assume the composition will not be explicit (e.g., there will be no explicit interface for every composed application but can be for a composed application someone decides to build an explicit interface for)

Hmm, I think they exist on the same level of virtuality - with regard to composition, I just mean that if you and I have both defined the same applications A, and B, we can compose them in the default way and receive a C = compose(A, B) which is the same C. If we compose them in a non-default way (perhaps creating additional transaction functions in the interface), we would need to communicate those transaction functions in order to agree on the same definition for the composed application.

@vveiln

Do we want some kind of structure here? How do we ensure that all of them are satisfied? Or how do we pick the ones to satisfy, if we don’t necessarily want all of them to be satisfied?

To be clear, not all of these resource logics (nor their associated resources) are necessary involved in every transaction - that’s up to the specific logics and transaction functions in question. For example, take a “two-token application” which consists of two tokens that can be interconverted with some fixed exchange ratio. This application would consist of two token resource logics (application logic) and transaction functions to mint, burn, and transfer each of tokens, plus to convert between the two (application interface). Only the convert transactions would typically involve both resource logics - mint, burn, and transfer would typically involve just one of them.

@vveiln

If a composed application logic is the union, it either implies that we assume the satisfaction of all resource logics at once (which would make sense, but just checking if we do) or we introduce a lot more variability for composed application logic instances, which sounds like a mess without specified logic enforcement rules

Hmm, I’m not quite sure that I follow this - applications are completely virtual, they do not imply any additional checks in the protocol - the resource machine should be entirely unaware of even the concept of an “application”. These definitions of applications are not proposing any changes in the resource machine abstractions or verification logic - only a specific way to define an “application” from the perspective of a developer or user writing resource logics and transaction functions.

[vveiln]

Diagrammed the account abstraction example (without example transactions)

[vveiln]

I think I might understand it better now. So, here is how I think about applications:

An application:

• an application resource logic (ignoring the interface here) defines how the application works,
• resources of the application kind comprise the state of the application.

Multiple logics can happen if:

• an application maps to a single resource kind and the resource logic that is embedded in the resources requires additional logic checks - in the past we talked a bit about what at the time was called VP hierarchy - the main logic can request other logics to be satisfied. In that case saying that application logic is a set of logics induces loss of information - we don’t specify there is hierarchy, but there is hierarchy that cannot even be modified (well, the way secondary logics are organised doesn’t matter, but the existence of the main logic does, i think)
• another option is if the application maps to multiple resource kinds, which i think is probably what we are talking about as it naturally includes composed applications as well, but I think I don’t fully understand how it works. Is it the same as in the account abstraction example, which requires multiple resource kinds logics of which bind them together to create some kind of higher-level abstraction? In that case, there is still hierarchy (token resource → message resource → account resource)

I’m struggling to imagine an application where there is no hierarchy (we might not be able to specify it completely, but the fact that some logic is the first one to be called). Assuming that there is always “the first” logic, can there be applications where “the first” logic is not unique? In that case I can assume the logic to be checked “first” is defined by the resource that was consumed/created

So I guess my point is that there seems always to be “the first” logic (can happen to be the only one in the hierarchy), which is determined by the consumed resource. The way I see it in the account abstraction example, there is linear hierarchy and the first logic is the token logic. If we don’t involve the token logic, a different application will be checked (“message authorisation application”), so in that sense logics of all three kinds are involved, but token logic is above the other two

[cwgoes]

@vveiln

I’m struggling to imagine an application where there is no hierarchy (we might not be able to specify it completely, but the fact that some logic is the first one to be called). Assuming that there is always “the first” logic, can there be applications where “the first” logic is not unique? In that case I can assume the logic to be checked “first” is defined by the resource that was consumed/created

Let me summarize my understanding of what you’re trying to get at here as:

• in order to make sense as a unified concept, the resource logics involved in an application need to reference each other in some sense
• often (or always), we could sort these references into some kind of hierarchy

Is that accurate?

I think that these are very helpful intuitions. Personally I’m not sure that I would conceptualize one of the resource logics as “first”. I think of resource logics w.r.t. applications more as a way to separate distinct parts of “application state” with distinct rules for how they can be updated, rules which may reference each other.

Sometimes, probably often, it will be possible to sort these references into a fully or partially ordered hierarchy - as in the “account abstraction” case - but this may not always hold, there’s nothing that prevents two application logics from simply referencing each other. I think that there is a good argument to be had, though, that if two resource logics always reference each other - such that transactions must always include and change both resources, they can never include only one - then these two resources should really just be one resource, and the resource logics, data, etc. should be combined. This is not something that we can enforce with the resource machine logic itself, but we could incorporate this criterion into our definition of applications, perhaps, and certainly into guidelines for developers of applications.

In particular, I think we can draw several useful notions from these intuitions:

From the intuition that resource logics involved in an application should reference each other in some way, I think that we can draw out definitions of application logic decomposition and application logic undecomposability:

Application logic decomposition refers to partitioning the set of logics L into two subsets L_1 and L_2, where:

• L_1 \cup L_2 = L
• L_1 \cap L_2 = \emptyset
• \forall l \in L_1, \forall l' \in L_2, \neg references(l, l') \land \neg references(l', l)
• references(a, b) is true if a includes a reference to b and false otherwise

For a particular application logic A, if A can be decomposed in this fashion for some L_1 and L_2, we say that A is decomposable. If A cannot be decomposed in this fashion, we say that A is undecomposable.

I think that this notion of undecomposable may accord with the intuition of an application being “bound together” that you mention - A is undecomposable if and only if the references between resource logics in A form a fully connected graph. If A is decomposable, the reference graph can be partitioned into (at least two) disconnected subgraphs.

From the intuition that resource references should generally form an orderable hierarchy, I think we can draw out definitions of resource dependence, resource independence, congruent application logic, and incongruent application logic (these last two names are very TBD), where:

• Two resources A and B are dependent if and only if no valid transitions exist which involve A but not B or B but not A.
• Two resources A and B are independent if and only if valid transitions exist which do not involve both A and B.
• A congruent application logic only allows for the creation of independent resources.
• An incongruent application logic allows for the creation of dependent resources.

I think that this concept of a congruent application logic may accord with the intuition of avoiding cycles in resource references, and being able to sort the references that do exist into some kind of hierarchy.

Let me know what you think.

[vveiln]

@cwgoes

in order to make sense as a unified concept, the resource logics involved in an application need to reference each other in some sense

I can imagine it not being necessary, some logics can exist in parallel (for composed applications, i assume), triggered when a certain application resource is created/consumed. But at the same time, there are always logics that are checked first (logically, i imagine it being parallel in practice). It is somewhat vague in my head (because it is very general and the examples I processed so far do not consider this), so I might be completely lost here. The diagram below describes how I imagine it:

@cwgoes

there’s nothing that prevents two application logics from simply referencing each other

In that case both of them can be “first”. I guess I think of these first logics as application state change entry points

@cwgoes

For a particular application logic A, if A can be decomposed in this fashion for some L_1 and L_2, we say that A is decomposable. If A cannot be decomposed in this fashion, we say that AAA is undecomposable.

So applying this to the example above, it is technically decomposable (logic YY vs the rest), but at the same time there are two entry points that cannot be decomposed because they share a sublogic. So from that perspective decomposability doesn’t correspond to entry points partition - I’m not sure it should have though

Applying the definition of dependence, independence, congruence and incongruence to my example above (to make sure I understand correctly):

• YY is independent from any other resource, (XX, XX_1) is also an independent pair (seems a bit counterintuitive. Do we want independency also require that there is no valid transition that involves both? in that case (XX, XX_1) would be neither dependent nor independent)
• (XX, XX_2) are dependent (well, in this example it isn’t actually clear if XX_2 is always triggered or optionally triggered, but let’s imagine it is always triggered - then there is no valid transition that involves XX but not XX_2)
• Application A logic is incongruent

@cwgoes

I think that this concept of a congruent application logic may accord with the intuition of avoiding cycles

Application A is incongruent but doesn’t have cycles

As a side note, thinking about this also made me think about sublogics that do not necessarily correspond to resources, but I imagine it easily being modified into the general case where the logic carrier resource is otherwise dummy (which might be unnecessary in practice but makes it easier to think of these cases in a unified way)

[cwgoes]

@vveiln

I can imagine it not being necessary, some logics can exist in parallel (for composed applications, i assume), triggered when a certain application resource is created/consumed. But at the same time, there are always logics that are checked first (logically, i imagine it being parallel in practice). It is somewhat vague in my head (because it is very general and the examples I processed so far do not consider this), so I might be completely lost here. The diagram below describes how I imagine it:

@vveiln

In that case both of them can be “first”. I guess I think of these first logics as application state change entry points

I think I understand better now - it should be the case that, for every transaction, we can calculate a partial order of the resource logics involved in the transaction, where a \le b iff. a checks the presence of a b (thus invoking resource logic b). If a \le b and b \le a, then a and b are “both first” (the mutual reference example); if a \le b but b does not reference a, then a \lt b; if neither a \le b nor b \le a, then a and b are unordered with respect to each other. Do you think this captures what you mean? Then, given particular actions (transaction functions), which perform particular operations, we can analyze which resource logics will be called (as you do in the diagram).

@vveiln

YY is independent from any other resource, (XX, XX_1) is also an independent pair (seems a bit counterintuitive. Do we want independency also require that there is no valid transition that involves both? in that case (XX, XX_1) would be neither dependent nor independent)

The notion of independency I defined above refers only to resources and resource logics, not actions (transitions) - we could also define a notion of independent transitions, I think, which would just be derived from the resource logic independence (two transitions A and B are independent iff. the only resources they can modify are themselves independent). I don’t think we want independence to require that there is no valid transition that involves both - then nothing would be independent, since two valid transactions can (for the moment, without negative/forall checks) always be combined into a single valid transaction.

@vveiln

(XX, XX_2) are dependent (well, in this example it isn’t actually clear if XX_2 is always triggered or optionally triggered, but let’s imagine it is always triggered - then there is no valid transition that involves XX but not XX_2)

Yes.

@vveiln

Application A logic is incongruent

If XX_1 always triggers XX_2 and XX_3 - yes.

@vveiln

Application A is incongruent but doesn’t have cycles

I think the relationships are:

• A congruent applications does not have cycles
• An incongruent application may have cycles

We could always define a notion of a really incongruent application where the only valid transitions are those which include all the resource logics - defined as such, really incongruent applications with more than one resource logic would always have cycles - but I don’t know how useful this distinction is .

[vveiln]

@cwgoes

Do you think this captures what you mean?

Generally I think it encapsulates a lot of knowledge, but I’m not sure it captures the notion of being “first”, and at first I thought that the first logic would be a minimal element (i.e., there is no b s.t. b \leq a), but then I started to wonder if it is possible to have a \leq b and both a and b being entry points, e.g. an application provides two actions:

1. requires triggering the logic chain a → b
2. requires triggering just the logic b

If that is possible then “first” != minimal, but I feel like there will be a resource kind conflict (where triggering logic b would be an action provided by a different application). But if it isn’t possible, then:

1. minimal logics are entry points
2. a logic can be triggered by different actions (like xx_1 in the diagram) only if it is not an entry point

Does it make sense?

[cwgoes]

@vveiln

If that is possible then “first” != minimal, but I feel like there will be a resource kind conflict (where triggering logic bbb would be an action provided by a different application).

I think this is possible, because the definition of which logics constitute an application is completely arbitrary - so I could create an application with logics a and b, and the two actions that you mention, and that would be a valid application, where “first” != minimal.

As we have defined them, applications are also non-exclusive, i.e. there could be:

• resource kinds r_1, r_2, r_3
• actions a_1, a_2, a_3
• an application app_0 with r_1, r_2, a_1, and a_2
• an application app_1 with r_2, r_3, a_2, and a_3

We could also define a notion of “intersecting” or “overlapping”, where two applications are intersecting iff. they share logics and/or actions (transaction functions) in common, and non-intersecting otherwise.

[cwgoes]

Notes on distributed partial evaluation:

• Must be added after updating transaction function definition
• Possible types
  • F : State -> (F | Tx) - unified type
  • F : State -> (F | (State -> Tx)), F_f : State -> Tx - separate types
  • Could consider adding an argument for what kind of evaluation is to be done
• What to do next?
  • @cwgoes to work on a forum post on this topic
  • Then discuss, clarify, once clear decide when/how to merge

[cwgoes]

Notes on calling conventions & encoding:

• @cwgoes to discuss with @mariari and write a post about this
• to also include encoding questions, specifically RLP / ABI / SSZ