# Goose v0.1.0 summary

**URL:** <https://forum.anoma.net/t/goose-v0-1-0-summary/1726>\
**Category:** Protocol Design\
**Created:** [July 3, 2025, 11:33am UTC](https://forum.anoma.net/t/goose-v0-1-0-summary/1726 "2025-07-03T11:33:35Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![Lukasz](https://avatars.discourse-cdn.com/v4/letter/l/0ea827/32.png) [@Lukasz](https://forum.anoma.net/u/Lukasz)\
**Post date:** [July 3, 2025, 11:33am UTC](https://forum.anoma.net/t/goose-v0-1-0-summary/1726/1 "2025-07-03T11:33:35Z")

</div>

This post provides a high-level description of GOOSE v0.1.0.

## AVM data structures

### Object

- `Object` in `Goose/Object.lean`
- concrete object representation
- consists of:
  - `classLabel` determines the object’s class
  - `quantity : Nat`
  - private fields
  - public fields

### Constructor

- `Class.Constructor` in `Goose/Class/Member.lean`
- represents a constructor of an object in a given class
- consists of:
  - `Args : Type`. Type of constructor arguments.
  - `created : Args -> Object` . Object created in a constructor call.
  - `extraLogic : Args -> Bool`. Extra constructor logic. It is combined with auto-generated constructor logic to create the complete constructor logic.

### Method

- `Class.Method` in `Goose/Class/Member.lean`
- represents a method of an object in a given class
- consists of:
  - `Args : Type`. Type of method arguments (excluding `self`).
  - `created : (self : Object) -> Args -> List Object`. Objects created in the method call.
  - `extraLogic : (self : Object) -> Args -> Bool`. Extra method logic. It is combined with auto-generated method logic to create the complete method logic.

### Member

- `Class.Member` in `Goose/Class/Member.lean`
- represents a class member: a constructor or a method.

### Class

- `Class` in `Goose/Class.lean`
- represents a class of objects
- consists of:
  - `classLabel` uniquely identifying the class (generated statically from class name).
  - `constructors : List Class.Constructor`. List of constructors.
  - `method : List Class.Method`. List of methods.
  - `extraLogic : (self : Object) -> Anoma.Logic.Args -> Bool`. Extra class-specific logic. The whole resource logic function for an object consists of the extra class-specific logic and the method and constructor logics.

## AVM → RM translation

### Object

Objects are translated to Resources. Currently, it’s a 1:1 translation.

- `classLabel` is stored in the `label` field.
- `quantity` is stored in `quantity`.
- Private fields are stored in the `value` field.
- Public fields are stored in associated App Data.
- The Resource Logic (RL) of the resource corresponding to the object is determined by the object’s class (see [Class](#Class) below). This way the resource kind (label + logic) determines the object class.
- The ephemerality of the resource is _not_ determined by the object. An object can map to either an ephemeral or non-emphemeral resource depending on how it is used in the action.

#### Resource data check

Resource data check `checkDataEq(res,obj)` compares a resource `res` against an object `obj`.

- `Class.Member.Logic.checkResourceData` in `Goose/Class/Member/Logic.lean`
- check `res.label == obj.classLabel`
- check `res.value` encodes the private fields of `obj`

### Constructor

#### Constructor call

Constructor calls are translated to single-action transactions. The action for a call to a constructor `constr` with arguments `args : constr.Args` is specified by the following.

- `Class.Constructor.action` in `Goose/Class/Translation.lean`
- Consumed resources:
  - one ephemeral resource corresponding to the created object `constr.created args`

- Created resources:
  - one non-ephemeral resource corresponding to the created object `constr.created args`

- App Data for each resource consists of:
  - member logic indicator:
    - for consumed ephemeral resource: the constructor logic
    - for created non-ephemeral resource: trivial logic (always true)

  - public fields of the created object
  - constructor call arguments `args`

#### Constructor logic

Constructor logic is the member logic executed for the consumed ephemeral resource in the transaction for constructor call. Constructor logic is implemented in `Class.Constructor.logic` in `Goose/Class/Translation.lean`.

Constructor logic has access to RL arguments which contain the following.

- `consumed : List Resource`. List of resources consumed in the transaction.
- `created : List Resource`. List of resources created in the transaction.
- App Data for the consumed ephemeral resource, which contains the constructor call arguments `args` (see [Constructor call](#constructor-call) above).

Constructor logic for a constructor `constr` performs the following checks.

- `consumed` contains exactly one resource `res` and `checkDataEq(res, constr.created args)` holds.
- `created` contains exactly one resource `res'` and `checkDataEq(res', constr.created args)` holds.
- `constr.extraLogic args` holds.

### Method

#### Method call

Method calls are translated to single-action transactions. The action for a call to a method `method` on `self : Object` with arguments `args : method.Args` is specified by the following.

- `Class.Method.action` in `Goose/Class/Translation.lean`
- Consumed resources:
  - one non-ephemeral resource corresponding to `self`

- Created resources:
  - non-ephemeral resource corresponding to the created objects `method.created self args`

- App Data for each resource consists of:
  - member logic indicator:
    - for consumed resource: the method logic
    - for created resources: trivial logic (always true)

  - public fields of the corresponding object (either `self` or a created object from `method.created self args`)
  - method call arguments `args`

#### Method logic

Method logic is the member logic executed for the consumed resource in the transaction for method call. The consumed resource `selfRes` corresponds to the `self` object in the method call. Method logic is implemented in `Class.Method.logic` in `Goose/Class/Translation.lean`.

Method logic has access to RL arguments which contain the following.

- `selfRes` consumed resource.
- `consumed : List Resource`. List of resources consumed in the transaction.
- `created : List Resource`. List of resources created in the transaction.
- App Data for the consumed resource `selfRes`, which contains:
  - public fields of the corresponding `self` object,
  - the method call arguments `args` (see [Method call](#method-call) above).  
The `self` object is re-created from `selfRes` and the public fields stored in App Data.

Method logic for a method `method` performs the following checks.

- `consumed` contains exactly one resource `selfRes` and `checkDataEq(selfRes, self)` holds.
- `created` contains resources corresponding to the created objects:
  - `created.length == method.created self args`,
  - `checkDataEq(res, obj)` holds pairwise for `(res, obj)` in `zip created (method.created self args)`.

- `method.extraLogic self args` holds.

### Class logic

Class logic is the RL associated with a class. The RL of a resource corresponding to an object is always the class logic of the object’s class. Class logic is implemented in `Class.logic` in `Goose/Class/Translation.lean`.

Class logic has access to RL arguments which contain the following.

- `selfRes` consumed resource.
- App Data for the consumed resource `selfRes`, which contains:
  - member logic indicator,
  - public fields of the corresponding `self` object.  
The `self` object is re-created from `selfRes` and the public fields stored in App Data.

Class logic for a class `cls` performs the following checks.

- Execute the member logic (constructor or method logic) based on the member logic indicator stored in App Data.
- Check `cls.extraLogic self` holds.

## Translation issues

- specs compliance:
  - currently, RM data structures are based on the transparent RM in Elixir, which is not fully specs-compliant

- computation of nonces and nullifiers:
  - known how to do, needs to be implemented
  - use mock functions to simulate the actual nullifier computation – the issue for the translation is where/how to store them and pass them around

- handling of nullifier key commitments:
  - needs conceptual work on how to represent them as identities/ownership on a higher level

- computation of delta proofs:
  - use mock functions to simulate the actual proof computation – the issue for the translation is where/how to store them and pass them around

- RL checks for the created case:
  - none for now, which is correct for the simple app examples we have, but not general enough
  - Yulia needs to think about this

- member logic indicators:
  - fine to put in App Data, assuming user not malicious
  - Yulia needs to think about the security implications more

- `quantity` field is not check in RLs, but should be

## Implemented example apps

- counter: `Apps/UniversalCounter.lean`

---

<div class="post-metadata">

**Author:** ![Lukasz](https://avatars.discourse-cdn.com/v4/letter/l/0ea827/32.png) [@Lukasz](https://forum.anoma.net/u/Lukasz)\
**Post date:** [July 29, 2025, 11:04am UTC](https://forum.anoma.net/t/goose-v0-1-0-summary/1726/2 "2025-07-29T11:04:18Z")

</div>

Summary of Goose v0.2.0 is now available at: [goose-lean/SUMMARY.md at main · anoma/goose-lean · GitHub](https://github.com/anoma/goose-lean/blob/main/SUMMARY.md)

Summaries for subsequent releases will be available directly in the goose-lean repository.

---

<div class="post-metadata">

**Author:** ![graphomath](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/graphomath/32/9_2.png) [@graphomath](https://forum.anoma.net/u/graphomath)\
**Post date:** [July 29, 2025, 11:40am UTC](https://forum.anoma.net/t/goose-v0-1-0-summary/1726/3 "2025-07-29T11:40:05Z")

</div>

![image](https://europe1.discourse-cdn.com/flex013/uploads/anoma1/original/2X/f/fc96615e8f41f79b6b71c4fe54b2da8a96e32d40.png)  
TL;DR