Juvix imports

module arch.node.engines.reads_for_environment;

import prelude open;
import arch.node.types.engine_environment open;
import arch.node.types.identities open;
import arch.node.engines.reads_for_messages open;

Reads For Environment

Overview

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

Mailbox states

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

syntax alias ReadsForMailboxState := Unit;

Local state

The local state of the Reads For Engine includes the evidence for reads_for relationships.

type ReadsForLocalState :=
  mkReadsForLocalState {
    evidenceStore : Set ReadsForEvidence;
    verifyEvidence : ReadsForEvidence -> Bool
  };

Timer Handle

syntax alias ReadsForTimerHandle := Unit;

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

Environment summary

ReadsForEnvironment : Type :=
  EngineEnvironment ReadsForLocalState ReadsForMailboxState ReadsForTimerHandle;

Example of a Reads For environment

readsForEnvironmentExample : ReadsForEnvironment :=
  mkEngineEnvironment@{
    name := "reads_for";
    localState :=
      mkReadsForLocalState@{
        evidenceStore := Set.empty;
        verifyEvidence := \ {_ := true}
      };
    mailboxCluster := Map.empty;
    acquaintances := Set.empty;
    timers := []
  };