Update RM specs with types

[jonaprieto]

T: The plan: for each page of the resource machine spec, we invent a topic name
X (e.g., the title of the page in question), create a new branch topic-X-rm and open a (draft) PR against #289; if applicable, a comparison with juvix-arm-spes is desirable.

Dependency DAG

Here is an attempt at making a comprehensive DAG of dependencies within the resource machine. This required some assumptions on my (AHartNtkn) part, so I may have identified things which should actually be different, but this should be correct enough to be useful. Note that this does not include application stuff (AppData, AppLogic, etc.) as that's somewhat ancillary and it's not clear how, if at all, that stuff would connect to the rest of the RM specs.

classDiagram
    %% Core Interfaces
    class IProvingSystem~VerifyingKey,ProvingKey,Instance,Witness,Proof~ {
        +prove(ProvingKey, Instance, Witness) Proof
        +verify(VerifyingKey, Instance, Proof) Bool
    }
    class IDeltaProvingSystem~VerifyingKey,ProvingKey,Instance,Witness,Proof~ {
        +aggregate(Proof, Proof) Proof
    }
    class ISet~T~ {
        +new() Set
        +new(List) Set
        +size(Set) Nat
        +insert(Set, T) Set
        +union(Set, Set) Set
        +intersection(Set, Set) Set
        +difference(Set, Set) Set
        +disjointUnion(Set, Set) Set
        +contains(Set, T) Bool
    }
    class IOrderedSet~T~
    class FixedSize~T,Arg~ {
        +bit_size: Int
        +new(Arg) T
        +equal(T, T) Bool
    }
    class Arithmetic~T,Arg~ {
        +add(T, T) T
        +sub(T, T) T
    }
    class Hash~T,Arg~
    class CommitmentAccumulator~Witness,CommitmentIdentifier,AccumulatedValue~ {
        +add(Accumulator, CommitmentIdentifier) Witness
        +witness(Accumulator, CommitmentIdentifier) Maybe Witness
        +verify(CommitmentIdentifier, Witness, AccumulatedValue) Bool
        +value(Accumulator) AccumulatedValue
    }
    class NullifierSet

    %% Core Data Structures
    class Resource {
        +logicRef: LogicHash
        +labelRef: LabelHash
        +valueRef: ValueHash
        +quantity: Quantity
        +isEphemeral: Bool
        +nonce: Nonce
        +nullifierKeyCommitment: NullifierKeyCommitment
        +randSeed: RandSeed
        +commitment() Commitment
        +nullifier(NullifierKey) Nullifier
        +kind() Kind
        +delta() DeltaHash
        +tag(consumed: Bool) Tag
    }
    class Action {
        +created: List Commitment
        +consumed: List Nullifier
        +resourceLogicProofs: Map Tag (LogicRefHash, PS.Proof)
        +complianceUnits: Set ComplianceUnit
        +applicationData: Map Tag (BitString, DeletionCriterion)
        +verify() Bool
        +delta() DeltaHash
    }
    class ComplianceUnit {
        +proof: PS.Proof
        +refInstance: ReferencedInstance
        +vk: PS.VerifyingKey
        +delta() DeltaHash
        +verify() Bool
    }
    class Transaction {
        +CMTreeRoots: Set CMtree.Value
        +actions: Set Action
        +deltaProof: DeltaProvingSystem.Proof
        +create(Set CMtree.Value, Set Actions) Transaction
        +compose(Transaction, Transaction) Transaction
        +verify() Bool
        +delta() DeltaHash
    }

    %% Implementation Classes
    class ResourceLogicProvingSystem
    class ComplianceProvingSystem
    class DeltaProvingSystem
    class OrderedSet
    class CMTree
    class NFSet
    class DeltaHash
    class TransactionFunction {
        +eval() Transaction
    }
    class TransactionFunctionVM {
        +eval(TransactionFunction, GasLimit) Transaction
    }
    class TransactionWithPayment {
        +stateTransitionFunction: TransactionFunction
        +paymentTransaction: Transaction
        +gasLimit: Arithmetic
    }

    %% Fixed Size Types
    class Nonce
    class RandSeed
    class NullifierKeyCommitment
    class NullifierKey
    class Quantity
    class Balance
    class LogicHash
    class LabelHash
    class ValueHash
    class Commitment
    class Nullifier
    class LogicRefHash

    %% Proof Related Types
    class ResourceLogicProofInstance {
        +tag: Tag
        +isConsumed: Bool
        +consumed: List Nullifier
        +created: List Commitment
        +applicationData: BitString
    }
    class ResourceLogicProofWitness {
        +consumed: OrderedSet (Resource, NullifierKey)
        +created: OrderedSet Resource
        +applicationInputs: Any
    }
    class ComplianceProofInstance {
        +consumed: List (NullifierRef, RootRef, LogicRefHash)
        +created: List (CommitmentRef, LogicRefHash)
        +unitDelta: DeltaHash
    }
    class ComplianceProofWitness {
        +consumed: OrderedSet Resource
        +consumed_nullifierKey: OrderedSet NullifierKey
        +consumed_cmtreePath: OrderedSet CMtreePath
        +consumed_commitment: OrderedSet Commitment
        +consumed_logicRefHash: OrderedSet LogicRefHash
        +created: OrderedSet Resource
        +created_logicRefHash: OrderedSet LogicRefHash
    }
    class DeltaProofInstance {
        +delta: DeltaHash
        +expectedBalance: Balance
    }
    class DeltaProofWitness {
        +resourceDeltaPreimages: List Resource
    }

    %% Inheritance/Implementation
    IProvingSystem --|> IDeltaProvingSystem
    IProvingSystem --|> ResourceLogicProvingSystem
    IProvingSystem --|> ComplianceProvingSystem
    IDeltaProvingSystem --|> DeltaProvingSystem
    ISet --|> IOrderedSet
    IOrderedSet --|> OrderedSet
    CommitmentAccumulator --|> CMTree
    Timestamp --> CMTree
    NFSet --|> NullifierSet
    FixedSize --|> Hash
    FixedSize --|> Arithmetic
    Hash --|> DeltaHash
    Arithmetic --|> DeltaHash

    LogicHash --> Resource
    LabelHash --> Resource
    ValueHash --> Resource
    Quantity --> Resource
    Nonce --> Resource
    NullifierKeyCommitment --> Resource
    RandSeed --> Resource
    Commitment --> Resource
    Nullifier --> Resource
    class Kind
    Kind --> Resource
    DeltaHash --> Resource
    Tag --> Resource
    Kind --> Resource

    Resource --> ComplianceProofWitness
    Resource --> NullifierSet
    Resource --> DeltaProofWitness

    %% Action Componenents
    Commitment --> Action
    Nullifier --> Action
    Tag --> Action
    IProvingSystem --> Action
    LogicRefHash --> Action
    DeletionCriterion --> Action
    ComplianceUnit --> Action

    %% Action interface reqs
    DeltaHash --> Action
    NullifierKey --> Action
    Resource --> Action

    IProvingSystem --> ComplianceUnit
    %%ReferencedInstance --> ComplianceUnit
    Commitment --> ComplianceUnit
    Nullifier --> ComplianceUnit
    DeltaHash --> ComplianceUnit

    Action --> Transaction
    CMTree --> Transaction
    DeltaProvingSystem --> Transaction
    DeltaHash --> Transaction

    Transaction --> TransactionFunction
    TransactionFunction --> TransactionWithPayment
    Transaction --> TransactionWithPayment
    Arithmetic --> TransactionWithPayment
    TransactionFunction --> TransactionFunctionVM

    OrderedSet --> ComplianceProofWitness

    Nullifier --> ComplianceProofInstance
    CMTree --> ComplianceProofInstance
    LogicRefHash --> ComplianceProofInstance
    Commitment --> ComplianceProofInstance

    CMTree --> ComplianceProofWitness
    NullifierKey --> ComplianceProofWitness
    Commitment --> ComplianceProofWitness
    LogicRefHash --> ComplianceProofWitness

    Predicate --> DeletionCriterion

    CMTree --> Transaction
    NullifierSet --> Transaction
    Action --> Transaction
    DeltaHash --> Transaction

    %% Fixed Size Type Implementation Dependencies
    Hash --> LogicHash
    Hash --> LabelHash
    Hash --> ValueHash
    Hash --> Commitment
    Hash --> Nullifier
    Hash --> Kind
    Hash --> LogicRefHash
    Hash --> CMTree

    Arithmetic --> Quantity
    Arithmetic --> Balance

    FixedSize --> Nonce
    FixedSize --> RandSeed
    FixedSize --> NullifierKeyCommitment
    FixedSize --> NullifierKey

    Balance --> DeltaProofInstance
    DeltaHash --> DeltaProofInstance
    NullifierKey --> Nullifier
    
    %% Input relationships (required for ResourceLogicProofInstance)
    Tag --> ResourceLogicProofInstance
    Nullifier --> ResourceLogicProofInstance
    Commitment --> ResourceLogicProofInstance
    Action --> ResourceLogicProofInstance
    Resource --> ResourceLogicProofInstance

    %% Output relationships (where ResourceLogicProofInstance is used)
    ResourceLogicProofInstance --> ResourceLogicProvingSystem
    
    %% Input relationships (required for ResourceLogicProofWitness)
    OrderedSet --> ResourceLogicProofWitness
    NullifierKey --> ResourceLogicProofWitness
    Resource --> ResourceLogicProofWitness

Loading

Definitions and Types Todo List

Types and functions which need to be implemented or reviewed. Note, it's not always clear what is going to be imported from where, so these checklists may overlap a bit.

• data/proof/delta.juvix.md
  • "Delta"? with following projections
    • delta. Defined as delta = sum(unit.delta() for unit in action.units for action in tx).
    • Function for "Transaction delta (computed from compliance unit deltas by adding them together)"
    • expectedBalance projection. Of type "Balance" which is not defined or mentioned elsewhere. Described as "delta's preimage's quantity component", which may imply a function checking this or computing this.
  • Function(s) to check "Balanced transactions have delta pre-image 0 for all involved kinds, for unbalanced transactions expectedBalance is a non-zero"
  • That witnesses are "Resource delta pre-images"?
  • Function to check "delta = sum(unit.delta() for unit in action.units for action in tx)"; see "### Constraints"
• data/proof/compliance.juvix.md:
  • "Compliance"? with projections
    • "consumed
      • Mentions NullifierRef, which isn't mentioned elsewhere,
      • Mentions RootRef, which is also not mentioned elsewhere.
      • Mentions LogicRefHash. LogicRefHash isn't described in detail, but it's needed for resources.
    • "created"
      • mentiones CommitmentRef, which isn't mentioned elsewhere.
  • "unitDelta = sum(r.delta() for r in consumed) - sum(r.delta() for r in created)"
  • Witnesses (possibly several types for different things being consumed/created, see list under "#### Witness")
  • function implementing "tag is recomputed from the object to verify that the tag is correct"
  • function to get "consumedResourceTagSet"
  • Algorithm described in "Each resource machine compliance proof must check the following"
  • Algorithm implementing "compliance proof sets can be simply united to provide a valid composed action compliance proof set."
• data/proof/logic.juvix.md
  • Projections listed in "#### Instance" (note, this requires figuring out the correct types as well, but is similar to Action in data/action.juvix.md)
    • tag (see data/resource/computable_components/tag.juvix.md)
    • consumed
    • created
    • applicationData
  • Witnesses for consumed resources
  • Witnesses for created resources.
  • Function to check "The instance and witness values are expected to correspond to each other: the first tag in the instance corresponds to the first resource object in the witness (and corresponds to the resource being checked), and so on. Note that the tag has to be recomputed from the object to verify that it indeed corresponds to the tag (this condition is included in the constraints)"
  • Function to check "Created commitment integrity: r.commitment() = cm"
  • The type NullifierKeyCommitment of nullifierKey.
  • Function to check "Consumed nullifier integrity: r.nullifier(nullifierKey) = nf"
  • Function(s) to check "Application constraints" (note: requires clarifying what those are in the first place)
• data/resource/computable_components/delta.juvix.md
  • "extraInput" type
  • Implement "r.delta() = deltaHash(r.kind(), r.quantity, extraInput)"
  • "unit.delta() = sum(r.delta() for r in unit.consumedResources) - sum(r.delta() for r in unit.createdResources)"
  • "action.delta() = sum(unit.delta() for unit in action)"
  • "transaction.delta() = sum(action.delta() for unit in transaction)"
  • Functions for "the delta can also be computed directly from resource deltas that comprise it, the way it is done for compliance units."
• data/resource/computable_components/kind.juvix.md
  • "kindHash" function
  • Function for "r.kind() = kindHash(r.labelRef, r.logicRef)"
• data/resource/computable_components/nullifier.juvix.md
  • Function to "publish nullifier"?
  • The nullifierHash function
  • function to check "r.nullifier(nullifierKey) = nullifierHash(nullifierKey, r)"
  • The "nullifier set" and
  • Storage of Nullifiers of consumed resources in nullifier set
  • Check that a resource is consumed only once.
  • "Every time a resource is consumed, it has to be checked that the resource existed before"
  • "Every time a resource is consumed, it has to be checked that the resource [...] has not been consumed yet"
• data/resource/computable_components/resource_commitment.juvix.md
  • the commitmentHash function
  • "r.commitment() = commitmentHash(r)"
  • commitment tree
  • storage of existing resource commitments in commitment tree
  • "The resource commitment is also used as the resource's address $r.addr$ in the content-addressed storage."
• data/resource/computable_components/tag.juvix.md
  • A tag is just either a commitment or a nullifier, and checking a tag means checking the nullifier if it's been consumed, and the commitment otherwise. Assuming the type in the file is correct, the checking function is all that needs implementing.
• data/resource/definition.juvix.md
  • Contains the type of the resource definition. Components require the following types;
  • LogicRef. LogicRef is a "LogicHash" which is "used to compute it should output the logic's verifying key and therefore is determined by the proving system used to compute resource logic proofs." No idea what this means, but implies some kind of function implementation.
  • LabelRef. LabelRef isn't described in the current files, but is implied to be a coproduct of tags indicating "fungibility domains".
  • ValueRef. Not described anywhere. Brief description indicates it may be nothing more than a hash of the "fungible data" of the resource. This implies functions gathering and hashing this data.
  • Quantity. Despite being called "Quantity", implying it's a type of quantity, the component of type quantity is described as "a number representing the quantity of the resource", meaning it should be a member of some kind of integral domain, presumably.
  • NullifierKeyCommitment. Part of nullifier as the type of nullifierKey.
  • Nonce. Nonce is not described anywhere. It's said to guarantee "the uniqueness of the resource computable components". Is it just and ID?
  • RandSeed
  • The final paragraph implies that, for several (every?) function operating on the resource objects, there are analogs operating on the shadow of the resource object existing within the state. Not sure what that's supposed to look like.
• data/action.juvix.md
  • Defines "Actions" type which require the following datatypes (mostly from other files)
    • Commitment (See data/resource/computable_components/resource_commitment.juvix.md)
    • Nullifier (See data/resource/computable_components/nullifier.juvix.md)
    • Tag (See data/resource/computable_components/tag.juvix.md)
    • LogicRefHash (See data/proof/compliance.juvix.md)
    • PS.Proof (/primitive_interfaces/proving_system/proof.juvix.md)
    • ComplianceUnit (See data/compliance_unit.juvix.md)
    • AppDataValueHash. AppDataValueHash Is not described in any detail, and it's unclear what it could mean.
    • DeletionCriterion. See section ## Data blob storage in "notes/storage.juvix.md", but it's not.
  • The note on "resourceLogicProofs" about recursivness implies a function implementing the described assumption.
  • Implement functions checking that (or have things constructed such that):
    • proofs created in the context of an action have access only to the resources associated with the action
    • A resource is said to be associated with an action if its commitment or nullifier is present in the action's created or consumed correspondingly
    • A resource is associated with exactly one action.
    • A resource is said to be consumed in the action for a valid action if its nullifier is present in the action's consumed list.
    • resource is said to be created in the action for a valid action if its commitment is in the action's created list.
  • if an action is valid and balanced, it is sufficient to create a balanced transaction.
  • Interface describes three functions;
    • create.
      • This requires a "NullifierKey" type, which is not described anywhere. Apparently different from NullifierKeyCommitment, and not the type of "nullifierKey".
      • Note the type of create is not consistent; in its second appearence it's said to take a CMtreePath along with every NullifierKey and Resource. CMtreePath is not mentioned outside of this, but presumably is related to "tree path" mentioned in notes/storage.juvix.md.
      • Implement algorithm for create according to steps described under "## create"
    • delta. Requires a "DeltaHash" type, see data/proof/delta.juvix.md.
      • action.delta() = sum(cu.delta() for cu in action.complianceUnits)
      • used to compute transactionDelta.
    • verify
      • Implement algorithm for verify according to steps described under "## verify"
  • "Resource logic proofs are created by ResourceLogicProvingSystem." ResourceLogicProvingSystem is not described anywhere. Based on the context of primitive_interfaces/proving_system/proving_system.juvix.md, this is likely just an instance of the proving system defined in primitive_interfaces/proving_system/proof.juvix.md.
  • Functions for calculating or checking the following, or guarantees by construction of;
    • For each resource consumed or created in the action, it is required to provide a proof that the logic associated with that resource evaluates to True given the input parameters that describe the state transition induced by the action.
    • The number of such proofs in an action equals to the amount of resources (both created and consumed) in that action, even if some resources have the same logics.
  • "Resource machine compliance proofs are created by ComplianceProvingSystem." ComplianceProvingSystem is not described anywhere. Based on the context of primitive_interfaces/proving_system/proving_system.juvix.md, this is likely just an instance of the proving system defined in primitive_interfaces/proving_system/proof.juvix.md.
• data/compliance_unit.juvix.md
  • ComplianceUnit type with three projections
    • proof. Requires PS.Proof (see /primitive_interfaces/proving_system/proof.juvix.md)
    • refInstance. Of type ReferencedInstance, which isn't defined, but see warning which describes it as a "PS.Instance" varient (see primitive_interfaces/proving_system/proof.juvix.md).
    • vk. Of type PS.VerifyingKey (see primitive_interfaces/proving_system/proof.juvix.md)
  • The note describes an algorithm for Referencing Merkle tree roots.
  • A "delta" projection is mentioned, and an algorithm for calculation is given in ## Delta.
  • #### Delta for computing balance describes a few algorithms for calculating "total balance for a compliance unit, action, or transaction".
  • Several functions from the second interface:
    • delta. Requires "DeltaHash" (see data/proof/delta.juvix.md)
    • created. Returns a "Commitment". (See data/resource/computable_components/resource_commitment.juvix.md)
    • consumed. Returns a "Nullifier". (See data/resource/computable_components/nullifier.juvix.md)
    • verify. Algorithmic connection to "ComplianceProvingSystem". ComplianceProvingSystem is not described anywhere. Based on the context of primitive_interfaces/proving_system/proving_system.juvix.md, this is likely just an instance of the proving system defined in primitive_interfaces/proving_system/proof.juvix.md.
• data/transaction.juvix.md
  • "Transaction" type with projections:
    • CMTreeRoots.
      • Mentiones the type "CMtree.Value"? This type isn't mentioned elsewhere. Perhapse this should be a parameter to the CMTree and transactions? See notes/storage.juvix.md
    • actions. Mentions the type of Actions (see data/action.juvix.md)
    • transactionDelta.
      • Mentions the type "DeltaHash.T", which isn't mentioned elsewhere and is hard to make heads or tails of.
      • Implement function for " It is computed from delta parameters of actions in that transaction."
    • deltaProof.
      • Mentions the type "DeltaProvingSystem.Proof". (see primitive_interfaces/proving_system/proving_system_delta.juvix.md), however, this type isn't mentioned, instead that file talks about "PS.Proof". Maybe this is a parameter of DeltaProvingSystem?
      • Implement functionality for "It makes sure that transactionDelta is correctly derived from the actions' deltas and commits to the expected publicly known value, called a balancing value."
  • Interface has three functions, along with algorithms described;
    • create
    • compose
    • verify
  • Implement check for "A transaction is executable if it is valid and transactionDelta commits to the expected balancing value."
• /notes/function_formats/transaction_function.juvix.md and transaction_function_vm.juvix.md (See topic-transaction-function branch)
  • Transaction function is described as a type of programs.
    • Support for READ_STORAGE
    • Support for DATA_BY_INDEX
    • Gas model
    • Eval function which performs execution (w/ an input context?). "eval(TransactionFunction, GasLimit) -> Transaction".
  • Implement listed examples. At least nock, maybe others.
• /notes/applications.juvix.md
  • Defines a type of Applications with thre projections
    • AppLogic
      • Is supposed to be a set of "resource logics" (no specific type is given), which is also a finite field?
    • AppWriteInterface. A TransactionFunction (see data/transaction.juvix.md)
    • AppReadInterface.
      • Defined as a set of things of type "ProjectionFunction". It then contradicts itself by asserting that ProjectionFunction is itself a term of type "AppState \rightarrow T", for an unspecified type, T. It then defines "AppState = AppResources \times AppData". AppResources is not defined anywhere, nor is it mentioned elsehwere. AppData is mentioned elsewhere, but it isn't defined anywhere.
  • The type "AppKinds \subseteq \mathbb{F}_{kind}" is described, but not used anywhere.
  • A description of application composition is described, which can be implemented as a function.
  • A description of application extension is described, which can be implemented as a function.
• notes/roles_and_requirements.juvix.md
  • Describes a number of "roles". I don't know how these should manifest in spec. Maybe as parameters for an abstract type describing a network as a whole. Maybe as a type class.
• notes/storage.juvix.md
  • A type, which is not given a name, is defined. Maybe "ARMState"? Contains following projections (none are given names);
    • A "Commitment accumulator". (See primitive_interfaces/commitment_accumulator.juvix.md). Also stated to map timestamps (part of CMtree) onto finite field elements.
    • A second "Commitment accumulator". Stated to map finite field x timestamp pairs onto finite field elements.
    • A "Nullifier set" (See data/resource/computable_components/nullifier.juvix.md). It also says that the nullifier set is a map from a finite field element to a finite field element?
    • A "Hierarchical index". A "Chained Hash set", whatever that is. It's stated to map tree paths to finite field elements. A "Tree path" isn't completely defined. The page uses the terms "tree path", "Merkle path", and "hierarchical index path" without clarifying the exact relation between these terms. Someone with expertise in Merkle trees might know what it's meant to be.
    • A "Data blob storage", which is defined to be a key-value store mapping finite field elements to (variable length byte array, deletion criterion) pairs.
      • The type of deletion criteria is a simple sum type with five options described in "## Data blob storage". However, these options implicitly make reference to types that aren't mentioned elsewhere. Mainly, blocks, "sig" over "data", and "predicates" which are "instantiated by options from this list". Hard to make sense of this.
  • The type "CMtree". The section describes a clear tree section allowing one to get a set of values from a timestamp of variable specificity.
  • The type "NFset" which seems to be an alternative name for what's been refered to as a "Nullifier Set" elsewhere. It supports basic set operations, but it's not clear what it's actually a set of. "NullifierKey"s? "NullifierKeyCommitment"s?
• primitive_interfaces/fixed_size_type/delta_hash.juvix.md
  • Delta hash, which should probably be a type class inheriting from basic arithmetic and hash/hashable type classes with implicit assumptions about homomorphisms. Such assumptions may be implemented as property-based tests in the future?
  • "An example of a function that satisfies these properties is the Pedersen commitment scheme". Implement this instance.
• primitive_interfaces/proving_system/proof.juvix.md
  • Defines a type of "proving system". It's made up of three types (maybe it should be a type class relating the types?)
    • A type "PS.Proof"
    • A type "PS.Instance"
    • A type "PS.Witness"
    • A type "PS.ProvingKey"
      • A function to produce "(x, w)" proof pair
    • A type PS.VerifyingKey;
    • A function Prove(pk, x, w): PS.ProvingKey \times PS.Instance \times PS.Witness \rightarrow PS.Proof
    • A function Verify(vk, x, \pi): PS.VerifyingKey \times PS.Instance \times PS.Proof \rightarrow Bool
  • There are several properties which are mentioned. Maybe these can be implemented via property-based testing macros in the future?
  • "The trivial scheme is one where computation is simply replicated" Implement this example;
  • "The trusted delegation scheme" implement this example (how would alt. party be formulated?).
  • "The succinct proof-of-knowledge scheme" implement this example.
• primitive_interfaces/proving_system/proving_system_delta.juvix.md
  • Defines the DeltaProvingSystem as an extension of the proving system type from primitive_interfaces/proving_system/proof.juvix.md. Makes sense to make it a type class inheriting from that.
    • Has an additional "proof agrigation" function of type (PS.Proof, PS.Proof) -> PS.Proof.
• primitive_interfaces/proving_system/proving_system.juvix.md
  • Mentions classification into three kinds of proof systems, one for compliance, one for resource logics, and one for deltas. The first two are just instances of the proving system from "primitive_interfaces/proving_system/proof.juvix.md", while the last is an instance of DeltaProvingSystem from primitive_interfaces/proving_system/proving_system_delta.juvix.md.
• primitive_interfaces/commitment_accumulator.juvix.md
  • Defines the "commitment accumulator" data structure (type class?) which is parameterized by three types, "Witness", CommitmentIdentifier, and AccumulatedValue. supports four functions;
    • add(Accumulator, CommitmentIdentifier) -> Witness.
    • witness(Accumulator, CommitmentIdentifier) -> Maybe Witness
    • verify(CommitmentIdentifier, Witness, AccumulatedValue) -> Bool
    • value(Accumulator) -> AccumulatedValue
  • There is a Merkle tree/CMTree instance mentioned. See notes/storage.juvix.md. Implement this instance.

[github-actions]

The typecheck failed. Please check the logs. However, the preview is available at https://specs.anoma.net/pr-289/.