# \[Proposal\] Scope refinement for resource machine report v2

**URL:** <https://forum.anoma.net/t/proposal-scope-refinement-for-resource-machine-report-v2/455>\
**Category:** RM\
**Created:** [January 26, 2024, 8:08am UTC](https://forum.anoma.net/t/proposal-scope-refinement-for-resource-machine-report-v2/455 "2024-01-26T08:08:49Z")\
**Posts on this page:** 20\
**Page:** 1

<div class="post-metadata">

**Author:** ![cwgoes](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/cwgoes/32/22_2.png) [@cwgoes](https://forum.anoma.net/u/cwgoes)\
**Post date:** [January 26, 2024, 8:08am UTC](https://forum.anoma.net/t/proposal-scope-refinement-for-resource-machine-report-v2/455/1 "2024-01-26T08:08:49Z")

</div>

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](https://forum.anoma.net/t/collective-curation-of-topics-to-go-in-resource-machine-report-v2/382) - 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](https://zenodo.org/records/10498991)):

- Balancing signature folding proofs (see [here](https://hackmd.io/@yulia/balancing-value-rm))
- Distributed partial evaluation analogy (see [here](https://forum.anoma.net/t/art-report-resource-machine/371/5)), 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](https://forum.anoma.net/t/simple-information-flow-control-for-partial-transactions/360) 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?

---

<div class="post-metadata">

**Author:** ![cwgoes](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/cwgoes/32/22_2.png) [@cwgoes](https://forum.anoma.net/u/cwgoes)\
**Post date:** [February 1, 2024, 11:15am UTC](https://forum.anoma.net/t/proposal-scope-refinement-for-resource-machine-report-v2/455/2 "2024-02-01T11:15:47Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![cwgoes](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/cwgoes/32/22_2.png) [@cwgoes](https://forum.anoma.net/u/cwgoes)\
**Post date:** [February 8, 2024, 8:26am UTC](https://forum.anoma.net/t/proposal-scope-refinement-for-resource-machine-report-v2/455/3 "2024-02-08T08:26:44Z")

</div>

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](https://specs.anoma.net/v1/architecture-2/ordering/types/transaction-candidate.html).
- 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](https://specs.anoma.net/v1/architecture-2/ordering/execution.html#executor-function).

---

<div class="post-metadata">

**Author:** ![cwgoes](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/cwgoes/32/22_2.png) [@cwgoes](https://forum.anoma.net/u/cwgoes)\
**Post date:** [February 9, 2024, 1:08pm UTC](https://forum.anoma.net/t/proposal-scope-refinement-for-resource-machine-report-v2/455/4 "2024-02-09T13:08:31Z")

</div>

**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

---

<div class="post-metadata">

**Author:** ![vveiln](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/vveiln/32/60_2.png) [@vveiln](https://forum.anoma.net/u/vveiln)\
**Post date:** [February 12, 2024, 9:55am UTC](https://forum.anoma.net/t/proposal-scope-refinement-for-resource-machine-report-v2/455/5 "2024-02-12T09:55:54Z")

</div>

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?

---

<div class="post-metadata">

**Author:** ![cwgoes](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/cwgoes/32/22_2.png) [@cwgoes](https://forum.anoma.net/u/cwgoes)\
**Post date:** [February 12, 2024, 10:10am UTC](https://forum.anoma.net/t/proposal-scope-refinement-for-resource-machine-report-v2/455/6 "2024-02-12T10:10:04Z")

</div>

> [@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)

---

<div class="post-metadata">

**Author:** ![cwgoes](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/cwgoes/32/22_2.png) [@cwgoes](https://forum.anoma.net/u/cwgoes)\
**Post date:** [February 13, 2024, 11:04am UTC](https://forum.anoma.net/t/proposal-scope-refinement-for-resource-machine-report-v2/455/7 "2024-02-13T11:04:32Z")

</div>

> 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.

---

<div class="post-metadata">

**Author:** ![cwgoes](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/cwgoes/32/22_2.png) [@cwgoes](https://forum.anoma.net/u/cwgoes)\
**Post date:** [February 13, 2024, 12:45pm UTC](https://forum.anoma.net/t/proposal-scope-refinement-for-resource-machine-report-v2/455/8 "2024-02-13T12:45:19Z")

</div>

> 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](https://forum.anoma.net/t/stored-data-format-resource-machine-storage/411/3), 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.

---

<div class="post-metadata">

**Author:** ![cwgoes](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/cwgoes/32/22_2.png) [@cwgoes](https://forum.anoma.net/u/cwgoes)\
**Post date:** [February 13, 2024, 2:09pm UTC](https://forum.anoma.net/t/proposal-scope-refinement-for-resource-machine-report-v2/455/9 "2024-02-13T14:09:08Z")

</div>

> 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](https://blog.ethereum.org/2014/01/15/slasher-a-punitive-proof-of-stake-algorithm) - 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.

---

<div class="post-metadata">

**Author:** ![vveiln](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/vveiln/32/60_2.png) [@vveiln](https://forum.anoma.net/u/vveiln)\
**Post date:** [February 15, 2024, 10:18am UTC](https://forum.anoma.net/t/proposal-scope-refinement-for-resource-machine-report-v2/455/10 "2024-02-15T10:18:54Z")

</div>

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?

2. 

> [@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

1. 

> [@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)

1. 

> [@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

---

<div class="post-metadata">

**Author:** ![cwgoes](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/cwgoes/32/22_2.png) [@cwgoes](https://forum.anoma.net/u/cwgoes)\
**Post date:** [February 15, 2024, 1:34pm UTC](https://forum.anoma.net/t/proposal-scope-refinement-for-resource-machine-report-v2/455/11 "2024-02-15T13:34:09Z")

</div>

> [@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.

---

<div class="post-metadata">

**Author:** ![vveiln](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/vveiln/32/60_2.png) [@vveiln](https://forum.anoma.net/u/vveiln)\
**Post date:** [February 15, 2024, 4:11pm UTC](https://forum.anoma.net/t/proposal-scope-refinement-for-resource-machine-report-v2/455/12 "2024-02-15T16:11:02Z")

</div>

Diagrammed the account abstraction example (without example transactions)

 ![image](https://europe1.discourse-cdn.com/flex013/uploads/anoma1/original/1X/1b6020713570f9fb0ec0d9ac018cf6410908339e.png)

---

<div class="post-metadata">

**Author:** ![vveiln](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/vveiln/32/60_2.png) [@vveiln](https://forum.anoma.net/u/vveiln)\
**Post date:** [February 16, 2024, 10:36am UTC](https://forum.anoma.net/t/proposal-scope-refinement-for-resource-machine-report-v2/455/13 "2024-02-16T10:36:17Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![cwgoes](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/cwgoes/32/22_2.png) [@cwgoes](https://forum.anoma.net/u/cwgoes)\
**Post date:** [February 16, 2024, 11:34am UTC](https://forum.anoma.net/t/proposal-scope-refinement-for-resource-machine-report-v2/455/14 "2024-02-16T11:34:28Z")

</div>

> [@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.

---

<div class="post-metadata">

**Author:** ![vveiln](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/vveiln/32/60_2.png) [@vveiln](https://forum.anoma.net/u/vveiln)\
**Post date:** [February 19, 2024, 10:43am UTC](https://forum.anoma.net/t/proposal-scope-refinement-for-resource-machine-report-v2/455/15 "2024-02-19T10:43:05Z")

</div>

> [@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:

 ![image](https://europe1.discourse-cdn.com/flex013/uploads/anoma1/original/1X/7763a8194a285746be86cbd3664b444399868967.png)

> [@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)

---

<div class="post-metadata">

**Author:** ![cwgoes](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/cwgoes/32/22_2.png) [@cwgoes](https://forum.anoma.net/u/cwgoes)\
**Post date:** [February 19, 2024, 12:50pm UTC](https://forum.anoma.net/t/proposal-scope-refinement-for-resource-machine-report-v2/455/16 "2024-02-19T12:50:41Z")

</div>

> [@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 😜 .

---

<div class="post-metadata">

**Author:** ![vveiln](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/vveiln/32/60_2.png) [@vveiln](https://forum.anoma.net/u/vveiln)\
**Post date:** [February 20, 2024, 12:35pm UTC](https://forum.anoma.net/t/proposal-scope-refinement-for-resource-machine-report-v2/455/17 "2024-02-20T12:35:17Z")

</div>

> [@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?

---

<div class="post-metadata">

**Author:** ![cwgoes](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/cwgoes/32/22_2.png) [@cwgoes](https://forum.anoma.net/u/cwgoes)\
**Post date:** [February 20, 2024, 2:19pm UTC](https://forum.anoma.net/t/proposal-scope-refinement-for-resource-machine-report-v2/455/18 "2024-02-20T14:19:50Z")

</div>

> [@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.

---

<div class="post-metadata">

**Author:** ![cwgoes](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/cwgoes/32/22_2.png) [@cwgoes](https://forum.anoma.net/u/cwgoes)\
**Post date:** [March 28, 2024, 10:24am UTC](https://forum.anoma.net/t/proposal-scope-refinement-for-resource-machine-report-v2/455/19 "2024-03-28T10:24:43Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![cwgoes](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/cwgoes/32/22_2.png) [@cwgoes](https://forum.anoma.net/u/cwgoes)\
**Post date:** [March 28, 2024, 10:29am UTC](https://forum.anoma.net/t/proposal-scope-refinement-for-resource-machine-report-v2/455/20 "2024-03-28T10:29:04Z")

</div>

Notes on calling conventions & encoding:

- @cwgoes to discuss with @mariari and write a post about this
- to also include encoding questions, specifically [RLP](https://ethereum.org/en/developers/docs/data-structures-and-encoding/rlp/) / [ABI](https://docs.soliditylang.org/en/develop/abi-spec.html) / [SSZ](https://ethereum.org/de/developers/docs/data-structures-and-encoding/ssz/)

[Next page](https://forum.anoma.net/t/proposal-scope-refinement-for-resource-machine-report-v2/455.md?page=2)