Notes from review of model

[cwgoes]

Notes from review by @cwgoes 2024.10.29 (not yet fully organized into tasks).

I started with reviewing only the overall model (not the transparent instantiation).

• We should align the identity types with those in the specs here (which are already in Juvix).
• I believe that the Reference type is wrong - in order to convert from a reference to the original value, you need not only the reference but also data, and the conversion should check that the data is the correct original value (by computing the hash, in practice).
• Why does verifyAction need to be a built-in? Shouldn't this call verify on some proof type with the appropriate inputs directly?
• We can get rid of InformationFlow entirely for now.
• Ditto for Preference (we can get rid of it)
• There's a lot of missing stuff here I think but we should write that in the specs first and then revisit this.

[heueristik]

We should align the identity types with those in the specs here (which are already in Juvix).

Agreed, we couldn't do this initially because we wanted to have compatibility with the node. It should be straightforward to replace these types.

I believe that the Reference type is wrong - in order to convert from a reference to the original value, you need not only the reference but also data, and the conversion should check that the data is the correct original value (by computing the hash, in practice).

trait
type Reference DataType RefType :=
  mkReference@{
    --- Computes the RefType from the DataType.
    to : DataType -> RefType;
    --- Computes the DataType from the RefType.
    from : RefType -> DataType
  };

This trait is there to mock the non-existent content-addressed BLOB storage (and is probably named very badly).
RefType is the address generated from the hashed content. to stores it in the blob storage and from fetches it from the blob storage. Does this resolve the issue?
Why do you need the original data when fetching it from the BLOB storage?
The correctness check after receiving the data makes sense though.

Why does verifyAction need to be a built-in? Shouldn't this call verify on some proof type with the appropriate inputs directly?

I cannot remember why we added it. Probably it happened accidentally.

We can get rid of InformationFlow entirely for now.
Ditto for Preference (we can get rid of it)

Removed in c24f43a

[heueristik]

When trying to bring in the Juvix definitions from the identity specs, I saw that the Commitment typename clashes:

A signature describing a type SignerType that can cryptographically sign (or credibly commit) to something (a Signable), forming a Commitment. Implementations should ultimately include, for example BLS keys, which should be able to sign anything that can be marshaled into a bitstring.

[...]

The Commitment type describes composed signatures, these are a MapCon from hashes of underlying verifiers to signatures (Commitment of underlyingVerifier)

There is an Identity.Commitment and a Resource.Commitment. It could be ok with using qualified names everywhere. Another option would be to use Signature instead, which is a bit more intuitive name (but maybe not accurate enough?).

[heueristik]

I ran into more problems when trying to move the Juvix definitions from the identity specs over (the task is https://github.com/orgs/anoma/projects/28 and the associated PR #10).
I opened a nspec issue https://github.com/anoma/nspec/issues/202

[cwgoes]

RefType is the address generated from the hashed content. to stores it in the blob storage and from fetches it from the blob storage. Does this resolve the issue?
Why do you need the original data when fetching it from the BLOB storage?
The correctness check after receiving the data makes sense though.

I see. I still think that this is the wrong interface for a "Reference" type, though, a "Reference" type should not imply some kind of storage, it's just a binding reference. The only thing you can do with a binding reference are:

• create a binding reference, from a piece of data
• check whether a binding reference matches a piece of data

We could add some other helper functions which look data up from the storage and check it against the binding reference (all in one function), but this shouldn't be part of the type itself. These storage fetches also need to be explicit in the transaction function, and we need to handle the case where they fail.

[heueristik]

I opened another nspec issue https://github.com/anoma/nspec/issues/204 because I don't know how to use or instantiate the identity definitions.
They seem to be not using the latest language features.

[cwgoes]

There is an Identity.Commitment and a Resource.Commitment. It could be ok with using qualified names everywhere. Another option would be to use Signature instead, which is a bit more intuitive name (but maybe not accurate enough?).

Hmm? Identity.Commitment is a type, Resource.Commitment is a function on a resource (computed field), right? If so, that's alright in principle. Would it cause issues with the Juvix?

In general, I think we want to avoid having two types with the same name (globally), but having some functions with the same name (as other functions, or as types) is fine.

[cwgoes]

I opened another nspec issue anoma/nspec#204 because I don't know how to use or instantiate the identity definitions. They seem to be not using the latest language features.

You should chat with @AHartNtkn about this, he wrote the most recent identity definitions in the specs.

[heueristik]

There is an Identity.Commitment and a Resource.Commitment. It could be ok with using qualified names everywhere. Another option would be to use Signature instead, which is a bit more intuitive name (but maybe not accurate enough?).

Hmm? Identity.Commitment is a type, Resource.Commitment is a function on a resource (computed field), right? If so, that's alright in principle. Would it cause issues with the Juvix?

In general, I think we want to avoid having two types with the same name (globally), but having some functions with the same name (as other functions, or as types) is fine.

Resource.Commitment is also a type in juvix-arm-specs that describes the commitment hash of a resource.
More specifically, it is a wrapper type and holds the underlying data type that an instantiator can pick. For the transparent RM the internal type is a ByteArray (see here).
The wrapper type adds type safety for app devs because they cannot confuse, let's say, a Commitment with a Nullifier that both are of type ByteArray in the transparent RM.

[heueristik]

I see. I still think that this is the wrong interface for a "Reference" type, though, a "Reference" type should not imply some kind of storage, it's just a binding reference. The only thing you can do with a binding reference are:

• create a binding reference, from a piece of data
• check whether a binding reference matches a piece of data

We could add some other helper functions which look data up from the storage and check it against the binding reference (all in one function), but this shouldn't be part of the type itself. These storage fetches also need to be explicit in the transaction function, and we need to handle the case where they fail.

I still struggle to see what you mean.

trait
type Reference DataType RefType :=
  mkReference@{
    --- Computes the RefType from the DataType.
    to : DataType -> RefType;
    --- Computes the DataType from the RefType.
    from : RefType -> DataType
  };

This is a Juvix trait (similar to a Rust trait). Maybe the type keyword is leading to confusion?
If I instantiate the Reference trait for, let's say Logic (which is done here), I can convert a Logic to a LogicRef by calling Reference.to (myLogic) and vice versa (Reference.from (myReferenceToALogicBlob)).

If this is not the issue, please bear with me.

[cwgoes]

Resource.Commitment is also a type in juvix-arm-specs that describes the commitment hash of a resource.
More specifically, it is a wrapper type and holds the underlying data type that an instantiator can pick. For the transparent RM the internal type is a ByteArray (see here).
The wrapper type adds type safety for app devs because they cannot confuse, let's say, a Commitment with a Nullifier that both are of type ByteArray in the transparent RM.

Ah, I see. In that case we probably need to either call the type ResourceCommitment, or just use the qualified Resource.Commitment, which is fine - this is not really a "new type" from the specs perspective, it's just an alias.

[cwgoes]

I see. I still think that this is the wrong interface for a "Reference" type, though, a "Reference" type should not imply some kind of storage, it's just a binding reference. The only thing you can do with a binding reference are:

• create a binding reference, from a piece of data
• check whether a binding reference matches a piece of data

We could add some other helper functions which look data up from the storage and check it against the binding reference (all in one function), but this shouldn't be part of the type itself. These storage fetches also need to be explicit in the transaction function, and we need to handle the case where they fail.

I still struggle to see what you mean.

trait
type Reference DataType RefType :=
  mkReference@{
    --- Computes the RefType from the DataType.
    to : DataType -> RefType;
    --- Computes the DataType from the RefType.
    from : RefType -> DataType
  };

This is a Juvix trait (similar to a Rust trait). Maybe the type keyword is leading to confusion? If I instantiate the Reference trait for, let's say Logic (which is done here), I can convert a Logic to a LogicRef by calling Reference.to (myLogic) and vice versa (Reference.from (myReferenceToALogicBlob)).

If this is not the issue, please bear with me.

I understand how to use the interface, I just think that:

• the type of from is definitely not possible to implement, because lookups from storage may sometimes fail
• I think it's better to put the lookups from storage in separate code, looking blobs up from storage should not be part of the reference type itself, since it's not part of what makes a binding reference a binding reference.

Specifically, say, I propose:

trait
type BindingReference DataType RefType :=
  mkBindingReference@{
    --- Computes the binding reference (RefType) from the data (DataType).
    compute : DataType -> RefType;
    --- Checks whether a particular piece of data matches a binding reference.
    check : RefType -> DataType -> boolean;
  };

and we can have a separate helper function lookupFromReference which uses a RefType to:

1. look up the data blob from storage,
2. check the reference against the blob (using the check function), and
3. return the value (or some error if the lookup or check failed)

[heueristik]

Specifically, say, I propose:

trait
type BindingReference DataType RefType :=
  mkBindingReference@{
    --- Computes the binding reference (RefType) from the data (DataType).
    compute : DataType -> RefType;
    --- Checks whether a particular piece of data matches a binding reference.
    check : RefType -> DataType -> boolean;
  };

and we can have a separate helper function lookupFromReference

Changed in 2f7b5b7