I have been reading the ARM specs to familiarise myself with them. As a result, I compiled a list of comments, and thought could be helpful to post it here.
Disclaimer: There is clearly a lot of effort invested on writing up this specs, so a big applause to everyone involved! Please do not take my comments the wrong way. It is constructive criticism 
I may have confused some things as well due to my newbie status.
Reviewed version: pull request pr-286 Anoma Specification
1. Main feedback
I have four main comments. They are related to the execution environment, the resource ownership, the level of abstraction of the specs, and the notation used.
1.1. Execution environment
This notion is quite important but it is not explicitly defined anywhere. I would have appreciated a page where this is explained in detail.
My understanding of the execution environment based on piecing together several excerpts of the specs. There are two execution environments, one on top of the another:
Bottom execution environment: structural and syntactic validation. It happens at the compliance unit level. It validates the syntax of the resources (correctness of commitments, nullifiers, etc). Also performs structural checks with respect to external components defining the anoma state (consumed resources have nullifiers committed in the tree of commitments)
Top execution environment: semantic validation. It happens at the action level. It validates resource logics, i.e. application-dependent predicates, of all resources involved in the action.
Both environments are linked (via hashes of predicates) to ensure that semantic and syntactic validation is for the same resources.
Why correctness of a nullifier is checked at both levels?
Composability. It probably deserves its own page (I only found a short paragraph here). A clear definition of the execution environment would help designing privacy-aware composition strategies.
1.2. Resource ownership
Whoever knows the nullifierkey owns the resource. There should be a mechanism that allows to delegate transactions that require matching without disclosing the nullifier to solvers.
According to this blog post Taiga had improved ZEXE delegation. Does RM have this feature, or does it plan to have it?
1.3. Level of abstraction
I understand the specification aims to be general and capture different types of instantiations. However, I feel they are a bit underspecified. It would help to have some sort of boundary for objects and interfaces differentiating transparent and shielded implementations. (Something similar to zcash specs.)
- What is shared with fixed meaning
- What is shared with mutable meaning
- What is unique to each instantiation
For example, logicRef is the hash of the predicate, or the verifying key of the associated SNARK?
1.4. Confusing notation
It is confusing to call everything a proof system.
- The trusted delegation proof system type is a signature scheme.
- The delta proof system is a commitment scheme, or a cryptographic accumulator.
I think that naming things properly gives clearer and simpler specifications, which leads to less buggy and easier to audit implementations. Also, with a proper naming of the building blocks it is more clear what type of cryptography the RM machines uses.
2. Other feedback
2.1 Resource logic definition
What is a resource logic/predicate according to the specs? I could not find a definition. If it is a function, what is its domain in terms of the defined data structures.
2.2. Nullifier generation
As defined, nullifier = Hash(resource,nullifierKey), it seems to not depend on the context of the compliance unit where it is created. If so, this may allow to create the same resource twice, i.e. in different compliance units. (The issue goes away by e.g. hashing also the consumed nullifiers present in the compliance unit, as in ZEXE.)
2.3. Deltas
Overall I found the abstraction a bit artifical. My opinion is that they should be described as homomorphic commitments. This is what they really are. For example, deltaHashcannot map to raw byte arrays. We need some sort of algebraic structure because there is a notion of arithmetic to derive deltas at diferent levels here. In the deltas calculation, what is really exploited is the length-reducing property of e.g. Pedersen hashes with commitment key \mathbf{ck}:=(g,h_1,\ldots,h_{n_u}) for some fixed binding generator g, and hiding generators h_i given by each kind of resources in u. For example:
- if m := r.quantity() the delta of a compliance unit u is c_u:= Pedersen_{\mathbf{ck}}(m;\mathbf{r}) for e.g.randomness vector \mathbf{r}=(1,0,\ldots,0)
- the delta of an action a with units u_1,u_2 and commitment keys \mathbf{ck}_1,\mathbf{ck}_2, with same binding generator g is c_a:=c_{u_1}+c_{u_2} = Pedersen_{\mathbf{ck}_1\cup\mathbf{ck}_2}(m_1+m_2,\mathbf{r}_1\cup\mathbf{r}_2)
- etc
2.4. Proof system definitions
Relates to this page.
Setup. I would include a setup algorithm to produce the proving/verifying keys. In the table and in the paragraph for Succinct PoK type (i.e. a proof system in the cryptographic sense) I would say a few words about the setup. Thus: Who or how the proving/verifying keys are generated, do we trust the key generators?
Succinctness. The notion of succinctness does not seem to be defined anywhere.
Universality. We say that for different statements different keys are needed. There are proof systems that can use the same keys for different statements – i.e. universal proof systems.
2.5. Ambiguity in type interface for proof system
The type/interface PS for a proof systems appears without further reference. It’s a bit confusing, and unclear its relation with ComplianceProvingSystem: the compliance unit interface uses PS, but compliance proofs are generated with ComplianceProvingSystem.
2.6. What is the statement of the resource logic?
I could not find definitions for RLinstance and to what correspond in resource objects (e.g. commitments etc)? Is there a notion of an RLwitness?