Add RM base interface module #19
Conversation
paulcadman
force-pushed
the
rm-base-interface
branch
from
460aa97
to
adcf4ff
Compare
There was a problem hiding this comment.
Yeah overall this looks mostly accurate, I believe some changes are required on our nock side for some functions but overall looks very close to both specs and what we have in the transparent code.
If you want me to review this for more "specs compliance", then I'd say we'd need clarity on compliance proof inputs for the verify function, but for the purpose this is nice
| --- INST_QUESTION: Can we assume that Kind, Commitment, Proof and | ||
| --- Delta types etc. are ;Nock.Atom;s so we don't need to make them builtin axioms? |
There was a problem hiding this comment.
I'd say yes for Kind Commitment and Proof
Delta Types I'm less sure of, how I represent them is pairing of the kind => quantity and I map it over to Nock.
My translation isn't perfect as instead of using signed numbers, I use [signed-bit number] which is important
I made an issue to track this particular format.
@agureev what are your thoughts on this bit?
| --- Application specific data needed to create resource logic proofs. | ||
| -- SPEC_QUESTION, INST_QUESTION: The RM instantiation does not enforce | ||
| -- this type, it accepts any data. Does this need to be specified? | ||
| appData : Set AppDataElement |
There was a problem hiding this comment.
The type of this likely isn't even a set in how you described it, it's defined as
{(k, (d, deletion_criterion)): k ∈ 𝔽ₖₑ, d ⊆ 𝔽ₐ}Meaning it's a map from k ---> AppDataValue.
Now take for instance
[mkAppDataElement key: 5 value: (mkAppDataValue value: 1 deletionCritera: 5);
mkAppDataElement key: 5 value: (mkAppDataValue value: 2 deletionCritera: 5)]
|> Set.from_list
|> mkAction ...
Now we have 2 keys of the same value. I think, because of this limitation of representing it via a Set, a list with no restrictions may make more sense in this representation.
But this is a good Specs question
There was a problem hiding this comment.
A lot more detail for this type is needed from the specs, as this implies certain storage behavior that changes how we deal with this quite drastically.
| -- SPEC_QUESTION, INST_QUESTION: The RM instantiation does not enforce | ||
| -- this type, it accepts any data. Does this need to be specified? | ||
| appData : Set AppDataElement |
There was a problem hiding this comment.
Unless for ZK reasons, I'd say it's morally anything the user wants in there.
If this were an OO language I'd say it's some Object, the Object may be a Set. This is surely overstepping to specify the exact representation unless it's for ZK reasons no?
| --- A set of roots of the commitment tree. | ||
| -- SPEC_QUESTION, INST_QUESTION: How do we obtain these roots? | ||
| roots : Set CommitmentTreeRoot; |
There was a problem hiding this comment.
You obtain them from the Indexer, you can query for the latest root
paulcadman
force-pushed
the
rm-base-interface
branch
from
e4ef630
to
2850cfe
Compare
This describes the interface exposed by the transparent instantiation of the RM specification.
Most Set operations can be done using the Juvix Set type. The only operations that are required for the Anoma interface are those which translate to/from the Stdlib Set type.
paulcadman
force-pushed
the
rm-base-interface
branch
from
dee44a7
to
8cdcfe2
Compare
This describes the interface exposed by the transparent instantiation of the RM specification.