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 := []
};