Goose v0.1.0 summary

Protocol Design
1

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 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 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 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
5 Likes