Juvix imports

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;

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.

Mailbox states

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

syntax alias SignsForMailboxState := Unit;

Local state

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

type SignsForLocalState :=
  mkSignsForLocalState {
    evidenceStore : Set SignsForEvidence;
    verifyEvidence : SignsForEvidence -> Bool
  };

Timer Handle

syntax alias SignsForTimerHandle := Unit;

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

Environment summary

SignsForEnvironment : Type :=
  EngineEnvironment SignsForLocalState SignsForMailboxState SignsForTimerHandle;

Example of a Signs For environment

signsForEnvironmentExample : SignsForEnvironment :=
  mkEngineEnvironment@{
    name := "signs_for";
    localState :=
      mkSignsForLocalState@{
        evidenceStore := Set.empty;
        verifyEvidence := \ {_ := true}
      };
    mailboxCluster := Map.empty;
    acquaintances := Set.empty;
    timers := []
  };