GOOSE: Good Object-Oriented System Experience

Anoma Research Topics |TECHNICAL REPORT GOOSE: Good Object-Oriented System Experience Lukasz Czajkaaand Jan Mas Roviraa aHeliax AG *E-Mail: [email protected], [email protected] Abstract We present GOOSE (Good Object-Oriented System Experience) – an object-oriented abstraction layer for the Anoma Resource Machine (Anoma RM) that lets developers write applications in terms of classes, objects, and methods while compiling to resource-based transactions and Resource Logics (RLs) that are correct by construction. GOOSE represents objects as RM resources and method calls as messages inducing actions. The RLs enforce class invariants and method logics, ensuring strong object interface safety: any valid transaction that modifies a GOOSE object, whether compiler-generated or handcrafted, must correspond to a sequence of permitted interface calls. We demonstrate the expressiveness and usability of this approach with a Kudos Bank case study that supports minting, transfers, checks, and auctions. Keywords: object-oriented programming ; Anoma ; Resource Machine ; (Received Month December 1, 2025; Published: December 19, 2025) Contents 1 Introduction 3 2 Motivation 5 2.1 Why not program in the ARM directly? ............ 5 2.2 How GOOSE helps ....................... 6 2.2.1 Interface security .................... 7 3 Anoma Resource Machine 7 3.1 Resources ............................. 7 3.1.1 Resource Logics ..................... 8 3.2 Transactions ........................... 9 3.2.1 Actions ......................... 9 3.2.2 Balance check ...................... 9 3.2.3 Examples ........................ 10 3.3 ARM Programs .......................... 11 DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |1–54 4 GOOSE Concepts 11 4.1 Objects .............................. 11 4.2 Messages ............................. 12 4.3 Classes .............................. 13 4.3.1 Class members ..................... 14 4.3.2 Example ......................... 15 4.4 Ecosystems and multi-methods ................. 17 4.5 Object upgrade .......................... 18 4.6 GOOSE Programs ........................ 18 4.6.1 Desugaring ....................... 19 5 Translation 21 5.1 Overview ............................. 22 5.1.1 Example ......................... 23 5.2 Objects .............................. 25 5.3 Tasks ............................... 26 5.4 Messages and member calls ................... 27 5.4.1 Message logics ..................... 27 5.4.2 Example ......................... 28 5.5 Interface security ........................ 31 5.6 Duality of GOOSE program code ................ 32 5.7 Class and member logics .................... 32 5.8 Constructor ........................... 33 5.8.1 Constructor call ..................... 33 5.8.2 Constructor message logic ............... 34 5.9 Destructor ............................ 35 5.9.1 Destructor call ..................... 35 5.9.2 Destructor message logic ................ 35 5.10 Method .............................. 36 5.10.1 Method call ....................... 36 5.10.2 Method message logic ................. 37 5.11 Upgrade ............................. 38 5.11.1 Upgrade call ....................... 38 5.11.2 Upgrade message logic ................. 38 5.12 Multi-method .......................... 38 5.12.1 Multi-method call .................... 38 5.12.2 Multi-method message logic .............. 39 6 Extended example: Kudos Bank 40 6.1 Opening a bank ......................... 40 6.2 Minting .............................. 41 6.3 Internal kudos transfers ..................... 41 DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |2 6.4 Check notes ........................... 42 6.5 Auction .............................. 43 7 Conclusion 45 8 Acknowledgements 46 References 46 A Implementation of GOOSE in Lean 4 46 A.1 Classes .............................. 47 A.2 Ecosystems ............................ 50 1. Introduction Anoma [GYB23] is a distributed operating system for intent-centric applications that unifies underlying blockchains into a single development environment, thereby mitigating the fragmentation of state and users that limits today’s decentralized applications. In the present paper, we show how this vision can be extended with an object-oriented interface. Smart contracts are the default organization principle for operating with digital assets, sometimes simplified to the idea of programmable money. For a long time, smart contract state has been accessible to the general public. Arbitrary private state transitions were available only for limited operations, e.g., the transfer of assets in a shielded pool. Anoma has developed the Anoma Resource Machine [KG24] (ARM or Anoma RM) to enable arbitrary shielded state transitions. The ARM is the part of the Anoma protocol responsible for creating, composing, and verifying transactions which create and consume resources. In this respect, its role in the Anoma protocol is similar to the role of the Ethereum Virtual Machine in the Ethereum protocol. At the level of the Anoma Resource Machine, any state is represented as immutable resources, and all state transitions are expressed as transactions that consume and create resources subject to a balance check and resourcespecific logic functions. This design provides a principled foundation for security and local reasoning about state updates. Still, it also exposes application developers to an unfamiliar, complex interface that is difficult to use directly. Even for simple applications, writing ARM transactions by hand requires careful management of resource labels, kinds, nonces, quantities, and resource logics. In contrast, mainstream application developers are accustomed to working in object-oriented programming (OOP) environments where state is encapsulated in objects and manipulated via methods. Such environments provide a natural way to factor application code into classes, objects, and method calls, DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |3 and they support reasoning in terms of domain concepts rather than underlying execution machinery. The Anoma Virtual Machine (AVM) [Hei25] proposes such an object-centric view for Anoma. However, the AVM defines an object-oriented model on a very abstract level, without specifying the details of its representation in the ARM. Bridging the gap between an OOP-style surface language and the ARM in a way that ensures security and composability is non-trivial. GOOSE (Good Object-Oriented System Experience) is our answer to this problem. GOOSE provides an object-oriented programming layer on top of the ARM. Developers write applications in a familiar style using classes, fields, constructors, and methods, and GOOSE compiles them into correctby-construction ARM transactions and resource logics. Conceptually, each object is represented by an RM resource, each method or constructor call translates to a sent message, and each message induces an RM action (a component of a transaction) together with the corresponding resource logics (RLs) that enforce the intended behaviour. With GOOSE, developers focus on domain-level behaviour, while the translation handles generating transactions and resource logics. The application developer does not need to know anything about the ARM. An important property of the GOOSE translation is that it guarantees object interface security. In other words, objects can only be modified in accordance with their public interface, and this is ensured also at the ARM level. Even if a malicious actor tries to submit a transaction directly, bypassing the GOOSE layer, they still cannot modify GOOSE objects (more precisely – their corresponding resources) in a way not allowed by the object interface. The only operations possible on an object are the ones defined by its methods. The GOOSE translation is compositional. Each method call is independently compiled to a separate action (a subdivision of an ARM transaction). These actions are composed into a single transaction that represents the translation of a GOOSE program. The generated RLs ensure that any transaction involving an object resource conforms to the object’s interface, i.e., that it implements one of the object’s methods. GOOSE programs that constitute object method bodies translate to both transactions and resource logics. The method code determines the updated object resource in a transaction for a method call. It also determines the constraints in the RL, which ensure the transaction’s conformance to the object interface. The GOOSE approach may therefore require compiling the same object-oriented code to two or more fundamentally different targets, because Anoma transactions and resource logics may be represented in two unrelated programming systems, e.g., Elixir for transaction submission and a zkVM for resource logics. DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |4 In this report, we present GOOSE programs in an object-oriented pseudocode, but GOOSE by itself is not a programming language. Rather, GOOSE provides a specification of an object-oriented framework and its translation to the Anoma Resource Machine. The GOOSE framework may be implemented in any programming language which is expressive enough to represent GOOSE concepts. In the appendix, we discuss an implementation of GOOSE in Lean 4. 2. Motivation Building Anoma applications [HR24] directly on the Anoma Resource Machine (ARM) [KG24] exposes developers to a low-level interface designed for precise control and safety of state updates. In practice, authoring applications directly on the ARM requires juggling many interconnected concepts: resources and their invariants (moderated by the resource logic functions), nonces, actions, delta proofs, compliance units, transactions, etc. – each of which is necessary for correctness, but collectively they create a high barrier to entry and slow down iteration. GOOSE (Good Object-Oriented System Experience) addresses this by providing an object-oriented programming layer on top of the ARM. The core idea is simple: developers write in a familiar OOP style – classes, fields, constructors, methods – and GOOSE compiles those programs to correct-byconstruction ARM transactions and resource logic functions. With GOOSE, programmers concentrate on application domain behaviour; the compiler takes on the mechanical and security-critical details that the ARM demands (e.g., nonce management, well-balanced transactions, generating resource logic functions that ensure objects can only be modified only through their public interface). 2.1. Why not program in the ARM directly? The ARM provides a low-level programming model unfamiliar to mainstream application developers, who would be better served with established objectoriented concepts. At the ARM level, an “object” is a resource carrying state and quantity, and correctness is enforced by both the resource logic and the balance checks: logic functions guard every admissible state transition and balance checks ensure that each transaction is balanced. Defining a new object and establishing its behaviour involves: • Designing the resource label. The resource label is part of the resource kind that determines whether the resources are treated as equivalent for the purpose of the balance check, i.e., of checking that the quantities of consumed and created resources match (see Section 3.1 and DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |5 Section 3.2.2). The resource label must therefore be chosen carefully so that balance checks have the desired effect. • Writing the resource logic function. Conceptually, this consists of anticipating all valid state transitions for the object and adding appropriate checks to guard them. It also involves parsing the resources in the action so that their values can be interpreted correctly in the logic checks. • Assembling transaction schemas that touch multiple resources, ensuring that consumed and created resources are balanced, nonces are fresh, and compliance units are formed correctly. This workflow is already error-prone for small applications, and its verbosity makes it unrealistic for large-scale application development. Furthermore, it demands an expert-level knowledge of the ARM. 2.2. How GOOSE helps GOOSE introduces an object-oriented layer and a surface syntax that looks and feels like a conventional OOP language. For instance, a simple GOOSE program could look like this: class Counter { var value: Nat constructor new(self: Counter) { self.value = 0 } method increment(self: Counter; by: Nat) { self.value += by } } def myProgram() { c = Counter.new() c.increment(1) c.increment(2) } This code above defines the Counter class, with a private field called value that carries a natural number, a single constructor that initializes the value to zero, and a method that increments the counter by a given amount. Finally, it defines a program — independent of the class — that creates a counter object and increments it twice by different values. GOOSE compiles myProgram to an Anoma transaction, ready to be submitted to an Anoma controller. DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |6 2.2.1. Interface security Apart from the familiar style of coding, GOOSE has another big advantage: interface security “for free”. In the above example, it is guaranteed that a Counter object can only be modified through its interface. For example, any transaction that attempts to decrement the value of a counter is rejected by the generated logic function, simply because no decrement method exists in the Counter class definition. Crucially, this remains true even for transactions crafted directly at the ARM level, without going through the GOOSE abstraction layer. In other words, there is effectively no way to circumvent the object’s interface. Interface security means that only the operations specified in an object’s interface can be performed on the object, exactly as defined. The generated logic functions ensure that any operation on a resource representing an object matches one of the operations (methods, constructors, destructors, multimethods) defined for the object’s class. The logic functions verify that the object is altered as specified by one of the operations, ensuring that all object fields are modified accordingly and that all nested calls are performed with the right arguments. See Section 5.5 for more details on how interface security is enforced by the GOOSE translation. 3. Anoma Resource Machine In this section, we describe the Anoma Resource Machine (ARM) to the extent necessary to understand the details of the translation employed by GOOSE. The full specification of the ARM is available in [KG24]. The version of the RM presented here is a simplification that omits some technical aspects not essential to GOOSE. The ARM is the part of the Anoma protocol that defines and enforces the rules for valid state updates. Its role in the Anoma protocol is similar to the role of the Ethereum Virtual Machine in the Ethereum protocol. A major difference is the novel ARM resource transaction model, which is neither the account nor the UTXO model. Two main concepts of the Anoma Resource Machine are resources and transactions. 3.1. Resources A resource is an atomic unit of RM state. Resources are immutable: each can be created and consumed only once. The current RM state is determined by the resources which were created but not yet consumed. A resource consists of the following. •logic: Hash of the associated resource logic. DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |7 •label: Together with the resource logic, determines the kind of the resource. •quantity: A natural number representing the quantity of the resource. •value: Data associated with the resource. •ephemeral: A boolean which determines whether the resource is ephemeral or persistent. Ephemeral resources are not stored in the RM state, and their existence is not checked when consumed. The resource kind is determined by the resource label and logic. Resources of the same kind are treated as equivalent in the balance check, described later. Speaking informally, we typically identify the kind of a resource with its label, since resources with the same label typically have the same resource logic function. The specification of the resource data structure above is simplified. In the ARM specification, resources also have fields for a nonce and a nullifierKeyCommitment. Nonce is a number used only once – it guarantees resource uniqueness. There can only be one resource with a given nonce in RM state. The nullifier key commitment corresponds to the nullifier key used to derive the resource nullifier. The resource nullifier is computed from the resource’s plaintext and the nullifier key. Publishing the resource nullifier by adding it to the nullifier set of RM state marks the resource as consumed [KG24]. The nonce and nullifierKeyCommitment fields are not essential for GOOSE, because we are only interested in properly using resource logics to encode valid object-state updates. In the GOOSE translation, only the nonce field plays a technical role in ensuring the uniqueness of object IDs. 3.1.1. Resource Logics Each resource has an associated resource logic (RL) – an implementation of a pure boolean function that is evaluated when the resource is created or consumed. The RL of each consumed or created resource needs to evaluate to true for a transaction to be valid. The RL of a resource 𝑅receives the following as input arguments: •self – the resource 𝑅for which the logic is invoked, •isConsumed – true if self is consumed in the action, •consumed – list of resources consumed in the action, •created – list of resources created in the action. A resource logic is a pure mapping from its arguments to a boolean value. It does not have access to any external environment, ARM state (beyond what is provided in the arguments) or IO operations. DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |8 3.2. Transactions A transaction specifies an RM state update. In particular, it specifies lists of consumed and created resources. Sums of quantities of consumed and created resources of the same kind must be equal for a transaction to be balanced. 3.2.1. Actions A transaction is partitioned into actions. An action determines the scope for the resource logics of resources in the action. For the purposes of GOOSE, the important aspect of an action is that it lists consumed and created resources. In the actual ARM for RISC Zero [BG+23], the structure of actions is more complex; they are divided into so-called compliance units, but these details are not essential to GOOSE, and we elide them here. 3.2.2. Balance check In the current design of the resource machine, each resource is assigned a quantity. The quantity preservation principle states that quantity must be preserved, i.e., in a transaction, the sum of quantities of all consumed resources must equal the sum of quantities of the created resources of the same kind. The balance check enforces the quantity preservation principle. Unbalanced transactions are not accepted by the ARM, and the state changes they specify cannot be performed. The scope of the balance check is the whole transaction, not only a single action. A constituent action may be unbalanced, as long as the enveloping transaction is balanced. For example, consider a transaction with a single action that contains the following resources. consumed • a resource of kind Dolphin with quantity 3 • a resource of kind Orange with quantity 2 • a resource of kind Orange with quantity 4 created • a resource of kind Dolphin with quantity 1 • a resource of kind Dolphin with quantity 2 DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |9 A member invariant has access to the same arguments as the corresponding member, plus the msg message argument. We have not yet defined the GOOSE programs which make up the bodies of class members. In member bodies in Example 1, we use some syntactic sugar that easily elaborates to GOOSE programs, as explained in Section 4.6. For the sake of readability, in our pseudocode examples, we take some liberties with how class members are presented. For example, in method definitions, the updated self object is not explicitly returned, but instead implicitly defined by imperative statements modifying the object’s private fields. Analogously, in constructor definitions, the created object is implicitly defined by imperative assignments to the object fields. Example 1. class Counter { var value: Nat var owner: UserId constructor new(self: Counter; owner: UserId) { self.value = 0 self.owner = owner } method increment(self: Counter; by: Nat) require(msg: Message) { msg.checkSignature(self.owner) } { self.value += by } } class TwoCounter { var count1: Counter var count2: Counter constructor new(self: TwoCounter; cnt1, cnt2: Counter) { self.count1 = cnt1 self.count2 = cnt2 } method incrementBoth(self: TwoCounter; n: Nat) { self.count1.increment(self.count2.value * n + self.count1.value) self.count2.increment(self.count1.value * n + self.count2.value) } } The Counter class represents an owned counter — only the owner of the counter is allowed to increment it. DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |16 The TwoCounter class has two fields count1 and count2 which store references to objects of type Counter. In all pseudocode we present, objects are always passed by reference. On the ARM level, object references are represented by object IDs. Accessing a field of an object (for example above in self.count2.value in incrementBoth) requires fetching the object data first. The translation from GOOSE programs to ARM programs inserts appropriate object fetches before accesses to object data. 4.4. Ecosystems and multi-methods So far, the concepts we presented allow us to consume and create only one object resource at a time. A class method operates on a single self object that is modified by the method. A method can call other methods on other objects, but it cannot specify that, e.g., two objects be destroyed together, unless there is a method to destroy each object separately. For a concrete example, consider the following Bank and Check classes. class Bank { // current account balance for each user var accounts: Map UserId Nat constructor new(self: Bank) { self.accounts = Map.empty () } } class Check { var owner: UserId var amout: Nat method transfer(self: Check; newOwner: UserId) require(msg: Message) { msg.checkSignature(self.owner) } { self.owner = newOwner } } We do not want to add a constructor to the Check class, because it should not be possible to create a check out of nothing. A check can only be created by a bank which needs to subtract the check amount from the account of the user issuing the check. Using the class methods presented so far, it is not possible to directly implement this functionality: a method for issuing a check would need to update the user’s balance and create a check, but it cannot create a check if the Check class does not have any constructors (which we do not want to be available in general). Multi-methods are a solution to this problem. In contrast to an ordinary class method, a multi-method operates on multiple self objects instead of DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |17 only one. It is possible to specify precisely which objects are destroyed, created, or updated. An ecosystem is a scope for classes and multi-methods. Each class and multi-method belongs to a unique ecosystem. A multi-method operates on multiple self arguments — objects of classes in the ecosystem. The self arguments are consumed by the multi-method. There may be other arguments provided besides the self arguments. An example multi-method for issuing a check follows. method issueCheck(bank: Bank; owner: UserId, amount: Nat) require(msg: Message) { msg.checkSignature(owner) assert bank.accounts[owner].amount >= amount } { bank.accounts[owner].amount -= amount create Check {owner = owner, amount = amount} } There is one self argument: bank. The corresponding bank object resource is consumed in the resulting transaction and an updated bank is created. The owner and amount arguments are additional non-self arguments. The issueCheck multi-method needs to be defined in the same ecosystem as Bank and Check. The multi-method creates a new Check without exposing aCheck constructor outside of the ecosystem. 4.5. Object upgrade As mentioned in Section 4.3, objects can be upgraded to objects with the same class and a higher version. For this to be allowed, the class of the object needs to be upgradeable. The upgrade mechanism is designed to enable future updates of objects to a newer version of their class. An arbitrary change to the object structure is allowed during the upgrade, provided the class name remains the same and the class version is higher. On the level of the ARM, an upgrade is a special message resource with no arguments or parameters – it is used solely to enforce the upgrade logic. The message logic ensures that the created object resource has the same class as the consumed object resource but with a higher version. 4.6. GOOSE Programs Having described all GOOSE concepts, we are ready to present GOOSE Programs more precisely. The pseudocode used for method bodies above is in fact syntactic sugar over GOOSE programs. GOOSE programs provide an object-oriented abstraction over ARM programs to which they are translated. An GOOSE program consists of a list of statements of the following form. DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |18 •objId = create Class.contructor args. Call a constructor to create a new object. •destroy destructor objId args. Call a destructor on an object with a given ID. •call method objId args. Call a method of a self object with a given ID. •multiCall multiMethod objIds args. Call a multi-method on self objects with given IDs. •upgrade objId to obj. Upgrade an object with a given ID objId to an object obj. An upgrade is permitted only to an object of the same class with a newer version. The new object obj replaces the upgraded one. The object’s ID is preserved. •obj = fetch objId. Fetch an object with a given ID. •invoke fn args. Invoke a function, i.e., a GOOSE subprogram. •return a. Return a given value a. GOOSE programs can also contain conditionals, matches and other control structures. We omit them here as they are not essential to the GOOSE translation. 4.6.1. Desugaring The pseudocode used in the examples is a more readable representation of GOOSE programs. The desugaring of this representation to the actual GOOSE programs described above is relatively straightforward. We clarify it here in more detail. • All objects are in fact object references represented by object IDs. For the sake of readability, we treat objects and object IDs interchangeably, leaving the fetch statements implicit. For example, referring to an object field obj.count requires fetching the object data first, so it is desugared to: objData = fetch obj objData.count • In the pseudocode, we use imperative statements modifying the fields of a self object instead of returning the new self object at the end of a method or a constructor. This is easily desugared to appropriate return statements. For example, the method DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |19 method increment(self: Counter; n: Nat) { self.count += n } is desugared to method increment(self: Counter; n: Nat) { selfObj = fetch self return {selfObj with count = selfObj.count + n} } •obj = MyClass.constructor(args) is desugared to: obj = create MyClass.constructor args When desugaring constructors, the self object is omitted from the arguments. Modifications to self in the body are replaced with returning the created object with appropriate field values. •obj.destructor(args) is desugared to destroy destructor obj args •obj.method(args) is desugared to call method obj args •multiMethod(obj1, .., objN, args) is desugared to multiCall multiMethod obj1 .. objN args •fn(args) is desugared to invoke fn args To illustrate the desugaring process, we present a desugared version of the example from Section 4.3.2. class Counter { var value: Nat var owner: UserId constructor new(owner: UserId) { return Counter {value = 0, owner = owner} } DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |20 method increment(self: Counter; by: Nat) require(msg: Message) { selfObj = fetch self invoke checkSignature msg selfObj.owner } { selfObj = fetch self return {selfObj with value = selfObj.value + by} } } class TwoCounter { var count1: Counter var count2: Counter constructor new(cnt1, cnt2: Counter) { return TwoCounter {count1 = cnt1, count2 = cnt2} } method incrementBoth(self: TwoCounter; n: Nat) { selfObj = fetch self count1Obj = fetch selfObj.count1 count2Obj = fetch selfObj.count2 call increment selfObj.count1 (count2Obj.value * n + count1Obj.value) // We need to update count1Obj because it was just incremented count1Obj = fetch selfObj.count1 call increment selfObj.count2 (count2Obj.value * n + count1Obj.value) } } 5. Translation In this section, we describe the GOOSE translation in detail. The core part of the translation is from GOOSE Programs to ARM programs, which is divided into three main stages: 1. move all object fetches to the front of the program, 2. create a transaction corresponding to the part of the program following the fetches, 3. create resource logics for all resources involved in the transaction, based on the code of class member bodies and invariants. We omit the desugaring described in the previous section and treat both versions of GOOSE programs interchangeably. DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |21 Before diving into details of how each GOOSE concept is represented in the ARM, we provide a general overview of the GOOSE translation. 5.1. Overview In essence, the GOOSE translation can be understood as creating one action per received message corresponding to a class member or multi-method call. This action contains: • consumed persistent object resources corresponding to self objects, • created persistent object resources corresponding to updated self objects, • consumed ephemeral message resource for the received message, • created ephemeral message resources for the nested calls, • consumed and created persistent object resources corresponding to the objects fetched in the body. The translation from GOOSE programs to ARM programs can be summarized by the following phases. 1. Move all object fetches to the beginning of the program. 2. Parametrize the program by values of new object IDs that need to be generated for constructor calls. 3. For each class member or multi-method call, create an action implementing the manipulations on self objects in the body. For example, a method increment in class Counter defined by method increment (n : Nat) { self.count += n } would result in an action with: • one consumed object resource corresponding to self, • one created object resource corresponding to self with the count field increased by n, • one consumed message resource for increment containing the n argument, • created message resources for all nested calls (none in this case), DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |22 • one consumed and one created object resource for each object fetched in the body (none in this case). 4. The previous points are applied recursively, resulting in a set of actions dependent on parameter values (fetched objects and generated object IDs). 5. The object fetches and ID generation at the beginning of the program are translated to queryResource and rand ARM program commands. 6. The actions are grouped into a single transaction, together with an action that sends the messages corresponding to the calls in the program. The submitTransaction command submits this transaction in the resulting ARM program. The message logics check that the created object resources correspond to the modifications of consumed object resources specified by the bodies of corresponding class members or multi-methods, e.g., for methods the consumed self object resource is correctly updated into the created object resource. The class logic checks that one of the following holds. 1. The self object is preserved (not modified). 2. There is exactly one consumed message resource, the self object is a recipient of the message and the message logic holds. The class logic also checks the class invariant for self. The resource logic of an object resource is the class logic for the class of the object. The resource logic of a message resource only checks if every recipient is present in the action when the message resource is consumed. 5.1.1. Example As an example, consider the following GOOSE program mutualIncrement, analogous to the incrementBoth method of TwoCounter from Section 4.3.2. def mutualIncrement(cnt1, cnt2: Counter, n: Nat) { cnt1.increment(cnt2.value * n + cnt1.value) cnt2.increment(cnt1.value * n + cnt2.value) } After desugaring, this program becomes: def mutualIncrement(cnt1, cnt2: Counter, n: Nat) { c1 = fetch cnt1 c2 = fetch cnt2 call increment cnt1 (c2.value * n + c1.value) c1 = fetch cnt1 call increment cnt2 (c1.value * n + c2.value) } DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |23 Moving object fetches to the front eliminates the fetch in the middle of the program in favour of updating c1 according to the Counter.increment method. def mutualIncrement(cnt1, cnt2: Counter, n: Nat) { c1 = fetch cnt1 c2 = fetch cnt2 call increment cnt1 (c2.value * n + c1.value) c1 = {c1 with value = c2.value * n + c1.value} call increment cnt2 (c1.value * n + c2.value) } This GOOSE program is translated into an ARM program performing the following. 1. c1 = queryResource cnt1 2. c2 = queryResource cnt2 3. submitTransaction tx where tx consists of two actions corresponding to the two calls and an action sending the call messages. The objects cnt1 and cnt2 are represented by object IDs, so c1.id is cnt1 and c2.id is cnt2. Action for the first call: • Consumed resources: –object resource for c1, –message resource for increment with recipient cnt1 and argument c1.value * n + c2.value. • Created resources: –object resource for: c1'= {c1 with value := c1.value + c1.value * n + c2.value} Action for the second call: • Consumed resources: –object resource for c2, –message resource for increment with recipient cnt2 and argument c2.value * n + c1'.value. • Created resources: DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |24 –object resource for: c2'= {c2 with value := c2.value + c2.value * n + c1'.value} Action sending the call messages: • Consumed resources: none. • Created resources: –message resource for increment with recipient cnt1 and argument c1.value * n + c2.value. –message resource for increment with recipient cnt2 and argument c2.value * n + c1'.value. In what follows, we describe in detail how each GOOSE concept is represented in the ARM and how GOOSE program statements are translated into ARM transactions. 5.2. Objects Objects are translated to Resources. Every object is translated to a single resource, but it may contain references to sub-objects which are translated to separate resources. References to sub-objects are represented by object IDs. A sub-object is just an object reference, so the same object can be a sub-object of multiple parent objects. Recall from Section 4.1 that: •class is stored in the label resource field, •id is stored in the value field, •quantity is stored in the quantity field, • private fields are stored in the value field. The resource logic of an object resource is determined by its class. This way, the resource kind (label & logic) determines the object class. The RL checks if the messages sent to the object correspond to class members or known multi-methods, and performs relevant message logic checks. The ephemerality of the resource is not determined by the object. An object can map to either an ephemeral or a persistent resource depending on how it is used in the action. For example, in an action implementing an object constructor, there are two resources corresponding to the created object: a consumed ephemeral object resource and a created persistent object resource. See also Section 3.2.3. DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |25 implemented by the action, i.e., the corresponding messages are sent with correct arguments. –The action contains created and consumed resources corresponding to fetched objects provided in message parameter values. This ensures that the objects in the message parameter values actually exist in the system with the given data. The ARM will check the existence of persistent consumed object resources with given data and ID, and the message logic checks that these correspond to the objects stored in the message resource as parameter values. The check for created object resources with the same data ensures that the transaction is balanced and the fetched objects are not arbitrarily modified. • The RL of the message resource checks — on consumption — that the object resource with the ID of the recipient object exists among the consumed resources in the action. This ensures that every message has a recipient in the action, and its logic cannot be ignored (the RL of the recipient object resource checks it). • The balance check in the ARM ensures that in the transaction, every message resource for a sent message must have a matching message resource for a received message. This ensures that every message sent (message resource created) for a nested call in the action for the sending object has a corresponding received message (message resource consumed) in a different action for the recipient object. 5.6. Duality of GOOSE program code A notable aspect of the translation is that the same body code is used to generate both the submitted transactions and the resource logics. The user can write ordinary object-oriented code without knowing or caring about how it maps to ARM concepts. This, however, may pose difficulties in implementing the GOOSE framework, because the ARM programs which submit the transactions and the resource logics need not even be written in the same programming language. The GOOSE approach may therefore require compiling the same object-oriented code to two or more fundamentally different targets. In the case of the Shielded Resource Machine, resource logics need to be compiled into zkVM bytecode, which imposes significant performance and functionality restrictions. 5.7. Class and member logics Class logic is the logic associated with a class. It is the logic invoked by the RL when an object of this class is consumed. Member logic may be invoked DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |32 by a class logic to check that the self object is a recipient of the message and the associated message logic holds. Class and member logics have access to RL arguments which contain the following. •selfRes. The consumed resource corresponding to the self object of the class. •consumed. List of resources consumed in the action. •created. List of resources created in the action. The self object is reconstructed from selfRes. Class logic checks that the class invariant holds, and one of the following is true. 1. The self object is preserved (not modified) in the action, i.e., selfRes is persistent, there is exactly one persistent created resource selfRes' with the ID self.id and selfRes'corresponds to self (i.e., selfRes and selfRes'represent the same object with equal fields). 2. The member logic holds for self, i.e., the self object is a recipient of the message and the message logic holds. More precisely: •consumed contains exactly one message resource for a message msg in the ecosystem of the class, •self.id is in msg.recipients, • The message logic for msg holds. 5.8. Constructor 5.8.1. Constructor call Constructor calls are translated to tasks. The task for a call to a constructor constr with arguments args is the composition of the tasks for nested calls in the constructor body with the constructor action specified by the following. See also Section 3.2.3. • Consumed resources: –one ephemeral object resource corresponding to the created object, i.e., the object returned by the constructor body, –one ephemeral message resource for the received constructor message, with message arguments set to args, DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |33 –persistent object resources corresponding to the objects fetched in the constructor body. • Created resources: –one persistent object resource corresponding to the created object, –ephemeral message resources for all messages sent in the constructor body (corresponding to nested calls), –persistent object resources corresponding to the objects fetched in the constructor body. The randomly generated IDs of created objects are ensured to be unique by making them equal to the nonce of the consumed ephemeral object resource. 5.8.2. Constructor message logic Constructor message logic is the logic associated with the constructor message. The message logic is checked in the RL of the recipient object resource on consumption. For a constructor message, the recipient object resource is the ephemeral consumed resource corresponding to the created object. Constructor message logic has access to RL arguments which contain the following. •msgRes. The resource of the constructor message. •consumed. List of resources consumed in the action. •created. List of resources created in the action. Constructor message logic for a constructor constr performs the following checks. •consumed contains: –one ephemeral object resource corresponding to the created object, –persistent object resources corresponding to the objects fetched in the constructor body. •created contains: –one persistent object resource corresponding to the created object, DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |34 –ephemeral message resources for all messages sent in the constructor body, with arguments matching the arguments to the nested calls, –persistent object resources corresponding to the objects fetched in the constructor body. •consumed and created may contain more message resources, but not any object resources other than the ones specified above. • The invariant of the constructor holds. 5.9. Destructor 5.9.1. Destructor call Destructor calls are translated to tasks. The task for a call to a destructor destr on self with arguments args is the composition of the tasks for nested calls in the destructor body, with the destructor action specified by the following. See also Section 3.2.3. • Consumed resources: –one persistent object resource corresponding to self, –one ephemeral message resource for the received destructor message, with message arguments set to args, –persistent object resources corresponding to the objects fetched in the destructor body. • Created resources: –one ephemeral object resource corresponding to self, –ephemeral message resources for all messages sent in the destructor body (corresponding to nested calls), –persistent object resources corresponding to the objects fetched in the destructor body. 5.9.2. Destructor message logic Destructor message logic is the logic associated with the destructor message. Destructor message logic has access to the following RL arguments. •msgRes. The resource of the destructor message. DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |35 •consumed. List of resources consumed in the action. •created. List of resources created in the action. Destructor message logic for a destructor destr performs the following checks. •consumed contains: –one persistent object resource selfRes corresponding to the self object, –persistent object resources corresponding to the objects fetched in the destructor body (matching the parameter values stored in the message). •created contains: –one ephemeral object resource selfRes'corresponding to the self object, –ephemeral message resources for all messages sent in the destructor body, with arguments matching those of nested calls, –persistent object resources corresponding to the objects fetched in the destructor body (matching the parameter values stored in the message). •consumed and created may contain more message resources, but not additional object resources. • The invariant of the destructor holds. 5.10. Method 5.10.1. Method call Method calls are translated to tasks. The task for a call to a method method on self with arguments args is the composition of the tasks for nested calls in the method body with the method action specified by the following. See also Section 3.2.3. • Consumed resources: –one persistent object resource for self, –one ephemeral message resource for the received method message, with message arguments set to args, DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |36 –persistent object resources corresponding to the objects fetched in the method body. • Created resources: –one persistent object resource corresponding to the updated self object, i.e., the updated object returned in the desugared method body (see Section 4.6.1), –ephemeral message resources for all messages sent in the method body, –persistent object resources corresponding to the objects fetched in the method body. 5.10.2. Method message logic Method message logic has access to the following arguments. •msgRes. The resource for the method message. •consumed. List of resources consumed in the action. •created. List of resources created in the action. Method message logic performs the following checks. •consumed contains: –one persistent object resource selfRes for self, –persistent object resources fetched in the method body. •created contains: –one persistent object resource selfRes'corresponding to the updated self object, –ephemeral message resources for all messages sent in the method body, –persistent object resources fetched in the method body (matching the parameter values stored in the message). • No other object resources appear in consumed or created. • The method invariant holds. DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |37 5.11. Upgrade 5.11.1. Upgrade call Upgrade calls are translated into tasks. The task for an upgrade of self to obj consists of the following. • Consumed resources: –one persistent object resource for self, –one ephemeral message resource for the received upgrade message. • Created resources: –one persistent object resource corresponding to obj. 5.11.2. Upgrade message logic Upgrade message logic has access to the following arguments. •consumed. List of resources consumed in the action. •created. List of resources created in the action. Upgrade message logic performs the following checks. •consumed contains exactly one persistent object resource selfRes corresponding to the self object. •created contains exactly one persistent object resource objRes corresponding to the obj upgraded object. •obj.id = self.id holds and the class of obj is the class of self with higher version. •consumed and created may contain additional message resources, but no other object resources. 5.12. Multi-method 5.12.1. Multi-method call Multi-method calls are translated into tasks. The task for calling multi-method multiMethod on a list selves of self objects with additional arguments args is the composition of the tasks for nested calls with the action defined by the following. • Consumed resources: DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |38 –persistent object resources for selves, –ephemeral object resources for constructed objects, –one ephemeral message resource for the multi-method message, –persistent object resources fetched in the body. • Created resources: –persistent object resources for assembled objects, –ephemeral object resources for destroyed objects, –persistent object resources for constructed objects, –ephemeral message resources for nested calls, –persistent object resources fetched in the body. 5.12.2. Multi-method message logic Multi-method message logic has access to RL arguments which contain the following. •msgRes. The resource of the method message msg, which contains the method call arguments args and parameter values vals. •consumed. List of resources consumed in the action. •created. List of resources created in the action. Given the number nof selves, we reconstruct the self objects from the first nresources in consumed, compute the multi-method result, and partition resources into the following lists. •disassembled. List of persistent object resources corresponding to initial values of the self objects that are updated in the multi-method body. •destroyed. List of persistent object resources corresponding to the self objects that are destroyed in the multi-method body. •constructedEph. List of ephemeral object resources corresponding to the objects created in the multi-method body. •fetchedConsumed. List of persistent object resources corresponding to the objects fetched in the multi-method body. Similarly, the created list is partitioned into the following. DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |39 •assembled. List of persistent object resources corresponding to final values of the self objects that are updated in the multi-method body. •destroyedEph. List of ephemeral object resources corresponding to the self objects that are destroyed in the multi-method body. •constructed. List of persistent object resources corresponding to the objects created in the multi-method body. •fetchedCreated. List of persistent object resources corresponding to the objects fetched in the multi-method body. Multi-method message logic performs the following checks. • The disassembled, assembled, destroyed, and constructed (persistent and ephemeral) resources correspond to the respective objects. • Resources in each partition have correct persistence/ephemerality, • Fetched resources (fetchedConsumed and fetchedCreated) match the objects fetched in the multi-method body provided in the parameter values vals stored in the message. • The multi-method invariant holds. 6. Extended example: Kudos Bank In this section, we present an extended example of the Kudos Bank application implemented in GOOSE. The example is intended to show the full capabilities of GOOSE. We use pseudocode syntax consistent with GOOSE pseudocode from earlier sections. Kudos bank application supports the following operations: • open and close a bank; • create tokens of their own denomination and store them in some bank; • transfer owned tokens to another user within the same bank; • issue, transfer, and deposit checks; • run an auction. 6.1. Opening a bank Any user can create a new bank, which they will own. A bank is an object that keeps track of the balances of its clients. Concretely, a bank consists of a map from public id (the client) to their account. An account maps each denomination to a quantity. A denomination is a public key, which identifies the originator of that denomination. DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |40 synonym Denom = PubId synonym Account = Map Denom Nat class Bank { var balances: Map PubId Account var owner: PubId constructor new(newOwner: PubId) { balances = emptyMap() owner = newOwner } method mint(self : Bank; originator: PubId, n: Nat) { require(msg: Message) { msg.checkSignature originator assert n > 0 } self.balances[originator][originator] += n } } 6.2. Minting A user can only mint tokens of their denomination. The mint method shown below has two parts, the body and the invariant. In the body, we increment the originator’s balance by ntokens of their denomination. In the invariant, we include security checks. In particular, we check that the originator has authorized with his signature the invocation of the method, in this case, minting kudos. class Bank { ... method mint(self : Bank; originator: PubId, n: Nat) { require(msg : Message) { msg.checkSignature originator assert n > 0 } self.balances[originator][originator] += n } } 6.3. Internal kudos transfers A user can transfer any amount of tokens that they own to another user within the same bank. In the body of the method, we adjust the balances of the sender and the receiver to reflect the transfer. In the invariant, we check DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |41 GOOSE IR (Lean) def Denom := PubId def Account := Map Denom Nat structure KudosBank where owner : PubId balances : Map PubId Account A core design choice of GOOSE is that the language of the GOOSE programs is embedded in the host language. This allows us to reuse all the language features of the host language, Lean. In practice, this means that when we write GOOSE programs, we can make use of Lean’s structures, inductive types, match expressions, let statements, and so on. Adding a method requires introducing a class label. Intuitively, a class labels is the interface of the class: it contains the types of its fields and the signatures of its constructors, methods, and destructors; but not the implementation. One could think of as an analogous to the headers file for C. Lean, Reference structure Label where name : String PrivateFields : SomeType ... The relevant part of the class label would be defined thus: GOOSE IR (Lean) def BankLabel : Class.Label where name := "KudosBank" PrivateFields := <KudosBank> ... We can now extend the class to add the new constructor. GOOSE constructor new(newOwner: PubId) { balances = emptyMap() owner = newOwner } In the class label definition we add ConstructorId and a function that DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |48 maps each constructor id to the type of its arguments: Lean, Reference structure Label where ... ConstructorId : Type ConstructorArgs : ConstructorId -> SomeType For our example, adding a constructor entails defining an enum type for the identifiers of the constructors and the function for the type of the arguments: GOOSE IR (Lean) inductive Constructors where | Open : Constructors def BankLabel : Class.Label where ... ConstructorId := Constructors ConstructorArgs := fun | Constructors.Open => <PubId> In order to add add methods and destructors to the label, an analogous change is required. We skip ahead to avoid unnecessary repetition. Let us proceed by showing how to implement a class method. We will use transfer as an example. DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |49 GOOSE class Bank { ... method transfer(self : Bank; owner: PubId, n: Nat, newOwner: PubId, denom: Denomination) { require(msg: Message) { msg.checkSignature owner assert n <= self.balances[owner][denom] assert n > 0 } self.balances[owner][denom] -= n self.balances[newOwner][denom] += n } } In the internal representation we define the body and the require section separately. In the actual codebase we named the require argument invariant, but we have renamed it here for consistency with the pseudocode syntax. GOOSE IR (Lean) def kudosTransfer : Method label Classes.Bank Methods.Transfer := defMethod KudosBank (body := fun (self : KudosBank) (args : TransferArgs) => return self.overBalances (fun b => b |> Balances.addTokens args.newOwner args.denom args.quantity |> Balances.subTokens args.oldOwner args.denom args.quantity) ) (require := fun (msg : Message label) (self : KudosBank) (args : TransferArgs) => 0 < args.quantity && msg.checkSignature args.oldOwner && args.quantity <= self.getBalance args.oldOwner args.denom) A.2. Ecosystems Like classes, ecosystems also have a label associated with them. In this label we specify which classes belong to it and what are the type signatures of its multi-methods. To specify the classes in the ecosystem, we specify an enum type and a function that maps each of the constructors to a class label. DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |50 Lean, Reference structure Ecosystem.Label where ... ClassId : Type classLabel : ClassId → Class.Label Specifying the type signatures of the multi-methods is done via these fields: Lean, Reference structure Ecosystem.Label where ... MultiMethodId : Type MultiMethodArgs : MultiMethodId → SomeType MultiMethodObjectArgNames : MultiMethodId → Type MultiMethodObjectArgClass : {f : MultiMethodId} → MultiMethodObjectArgNames f → ClassId The fields above contain the following information: •MultiMethodId contains an enum type that enumerates all the multimethod ids. •MultiMethodArgs maps each multi-method id to the type of its nonobject arguments. •MultiMethodObjectArgNames maps each multi-method id an enum type that has a constructor for each object argument. Each one of these constructors represents an argument name. •MultiMethodObjectArgClass maps each argument name to an object class id. Let us make it concrete by using the issueCheck multi-method as an example. To facilitate readability we copy the code below. DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |51 GOOSE method issueCheck(bank: Bank; owner: UserId, amount: Nat) require(msg: Message) { msg.checkSignature(owner) && bank.accounts[owner].amount >= amount } { bank.accounts[owner].amount -= amount create Check {owner = owner, amount = amount} } In the arguments section we first specify the object arguments and then the rest. They two categories are separated by a semicolon. In this case we have a single object argument, so we would have: GOOSE IR (Lean) inductive IssueCheck.ClassArgNames where | bank def label : AVM.Ecosystem.Label where ... MultiMethodObjectArgNames := fun | .IssueCheck => IssueCheck.ClassArgNames For the non-object arguments: GOOSE IR (Lean) structure IssueCheck.Args where denomination : Denomination owner : PublicKey quantity : Nat def label : AVM.Ecosystem.Label where ... MultiMethodArgs := fun | .IssueCheck => IssueCheck.Args Then, to implement the issueCheck multi-method we use the defMultiMethod helper function. The important arguments are: •argsInfo: The relevant instances for the object arguments. •require: A boolean precondition that must be satisfied. Equivalent to DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |52 the require argument in the class method. •body: The actual implementation of the multi-method. The arguments argsInfo and require can be provided straightforwardly: GOOSE IR (Lean) def issueCheck : @Ecosystem.MultiMethod label .IssueCheck := defMultiMethod label MultiMethods.IssueCheck (argsInfo := fun | .bank => { type := KudosBank, isObjectOf := KudosBank.instIsObjectOf }) (require := fun msg selves args => let bank := selves .bank msg.checkSignature args.owner && 0 < args.quantity && args.quantity <= bank.getBalance args.owner args.denomination) (body := ...) In order to explain the body argument we first need to understand the return type of a multi-method and some related types: Lean, Reference structure MultiMethodResult {lab : Ecosystem.Label} (multiId : lab.MultiMethodId) where argDeconstruction : multiId.ObjectArgNames → AVM.DeconstructionKind assembled : Assembled argDeconstruction constructed : List AnObject inductive DeconstructionKind where | Destroyed | Disassembled structure Assembled {label : Ecosystem.Label} {multiId : label.MultiMethodId} (argDeconstruction : multiId.ObjectArgNames → DeconstructionKind) where withOldUid : (arg : multiId.ObjectArgNames) → argDeconstruction arg = .Disassembled → Option (ObjectData arg.classId) withNewUid : List SomeObjectData DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |53 The fields in MultiMethodResult mean the following: •argDeconstruction: For each object argument we specify how it should be deconstructed. There are two options; if it is destroyed, an ephemeral resource is automatically inserted to satisfy the balance contraint. If it is disassembled, the object is meant to be balanced by one or more created objects. The most common case for disassembly is to update the data in an object. •assembled: Contains the created objects. The withOldUid defines the subset of the dissembled objects that should preserve their original object id. The objects in the withNewUid list will be assigned fresh ids. •constructed: A list of objects to be created with fresh ids. Additionally, ephemeral consumed objects will be added to balance the transaction. Finally, we can provide the body argument. In our example, we update the balances in the bank, which preserves the object id. Also, a new check object is constructed. GOOSE IR (Lean) def issueCheck : @Ecosystem.MultiMethod label .IssueCheck := defMultiMethod label MultiMethods.IssueCheck (argsInfo := ...) (require := ...) (body := fun selves args => return { assembled := { withOldUid arg _ := match arg with | .bank => let bank':= (selves .bank).overBalances (fun b => b |> Balances.subTokens args.owner args.denomination args.quantity) some { obj := bank', isObjectOf := KudosBank.instIsObjectOf } withNewUid := [] } argDeconstruction := fun | .bank => .Disassembled constructed := [{ denomination := args.denomination owner := args.owner quantity := args.quantity : Check }]}) DOI: 10.5281/zenodo.17966813 Anoma Research Topics |December 19, 2025 |54