module arch.system.types.state;

import prelude open;
import arch.system.types.nullifier open;
import arch.system.types.commitmenttree open;

axiom CommitmentAccumulator : Type;

axiom DataBlobStorage : Type;

axiom EqDataBlobStoragea : Eq DataBlobStorage;

instance
EqDataBlobStorage : Eq DataBlobStorage := EqDataBlobStoragea;

axiom OrdDataBlobStoragea : Ord DataBlobStorage;

instance
OrdDataBlobStorage : Ord DataBlobStorage := OrdDataBlobStoragea;

type State :=
  mkState@{
    -- commitmentAccumulator {A : Type} {{CommitmentTreeOps A CTree CTreePath}} : A ;
    -- secondCommitmentAccumulator : CommitmentAccumulator;
    nullifierSet : Set Nullifier;
    dataBlobStorage : DataBlobStorage;
  -- hierarchicalIndex : HierarchicalIndex;
  };

deriving instance
stateEq : Eq State;

deriving instance
stateOrd : Ord State;