module arch.node.engines.signs_for_environment;

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

Signs For Environment¶

Overview¶

The Signs For Engine environment maintains the state necessary for managing signs_for relationships between identities, including storing evidence submitted by clients.

axiom verifyEvidence : SignsForEvidence -> Bool;

Mailbox states¶

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

SignsForMailboxState¶

syntax alias SignsForMailboxState := Unit;

Local state¶

The local state of the Signs For Engine includes the evidence for signs_for relationships.

SignsForLocalState¶

type SignsForLocalState :=
  mkSignsForLocalState@{
    evidenceStore : Set SignsForEvidence;
  };

Timer Handle¶

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

SignsForTimerHandle¶

syntax alias SignsForTimerHandle := Unit;

The Signs For Environment¶

SignsForEnv¶

SignsForEnv : Type :=
  EngineEnv
    SignsForLocalState
    SignsForMailboxState
    SignsForTimerHandle
    Anoma.Msg;

Instantiation¶

signsForEnv : SignsForEnv :=
  mkEngineEnv@{
    localState :=
      mkSignsForLocalState@{
        evidenceStore := Set.empty;
      };
    mailboxCluster := Map.empty;
    acquaintances := Set.empty;
    timers := [];
  };