module arch.node.engines.commitment_environment;

import prelude open;
import arch.node.engines.commitment_messages open;
import arch.node.types.crypto open;
import arch.node.types.engine_environment open;
import arch.node.types.identities open;
import arch.node.types.messages open;
import arch.node.types.anoma_message as Anoma open;

Commitment Environment¶

Overview¶

The Commitment Engine environment maintains the state necessary for generating commitments (signatures) for a specific identity. It includes the identity's signing capabilities and any necessary signing keys or handles.

Mailbox states¶

The Commitment Engine does not require complex mailbox states. We define the mailbox state as Unit.

CommitmentMailboxState¶

syntax alias CommitmentMailboxState := Unit;

Local state¶

The Commitment engine is statless.

CommitmentLocalState¶

syntax alias CommitmentLocalState := Unit;

Timer Handle¶

The Commitment Engine does not require a timer handle type. Therefore, we define the timer handle type as Unit.

CommitmentTimerHandle¶

syntax alias CommitmentTimerHandle := Unit;

The Commitment Environment¶

CommitmentEnv¶

CommitmentEnv : Type :=
  EngineEnv
    CommitmentLocalState
    CommitmentMailboxState
    CommitmentTimerHandle
    Anoma.Msg;

Instantiation¶

axiom dummyExternalIdentity : ExternalIdentity;

axiom dummyIDBackend : Backend;

axiom dummySigningKey : SigningKey;

commitmentEnv : CommitmentEnv :=
  mkEngineEnv@{
    localState := unit;
    mailboxCluster := Map.empty;
    acquaintances := Set.empty;
    timers := [];
  };