Skip to content
Juvix imports

module arch.node.engines.reads_for_behaviour;

import prelude open;
import arch.node.types.messages open;
import Data.Set.AVL open;
import Stdlib.Data.List.Base open;
import Stdlib.Trait.Ord open;
import Stdlib.Data.Bool.Base open;
import arch.node.types.engine_behaviour open;
import arch.node.types.engine_environment open;
import arch.node.types.identities open;
import arch.node.engines.reads_for_messages open;
import arch.node.engines.reads_for_environment open;
import arch.node.types.anoma_message open;

Reads For Dynamics

Overview

The behavior of the Reads For Engine define how it processes incoming messages and updates its state accordingly.

Action labels

type ReadsForActionLabel :=
| DoReadsForQuery {
externalIdentityA : ExternalIdentity;
externalIdentityB : ExternalIdentity
}
| DoSubmitEvidence {evidence : ReadsForEvidence}
| DoQueryEvidence {externalIdentity : ExternalIdentity};

DoReadsForQuery

DoReadsForQuery { externalIdentityA : ExternalIdentity; externalIdentityB : ExternalIdentity }

This action label corresponds to processing a reads_for query.

DoReadsForQuery action effect

This action does the following:

Aspect Description
State update The state remains unchanged.
Messages to be sent A ReadsForResponse message is sent back to the requester.
Engines to be spawned No engine is created by this action.
Timer updates No timers are set or cancelled.

DoSubmitEvidence

DoSubmitEvidence { evidence : ReadsForEvidence }

This action label corresponds to submitting new reads_for evidence.

DoSubmitEvidence action effect

This action does the following:

Aspect Description
State update If the evidence doesn't already exist and is valid, it's added to the evidenceStore in the local state.
Messages to be sent A SubmitReadsForEvidenceResponse message is sent back to the requester.
Engines to be spawned No engine is created by this action.
Timer updates No timers are set or cancelled.

DoQueryEvidence

DoQueryEvidence { externalIdentity : ExternalIdentity }

This action label corresponds to querying reads_for evidence for a specific identity.

DoQueryEvidence action effect

This action does the following:

Aspect Description
State update The state remains unchanged.
Messages to be sent A QueryReadsForEvidenceResponse message is sent back to the requester.
Engines to be spawned No engine is created by this action.
Timer updates No timers are set or cancelled.

Matchable arguments

type ReadsForMatchableArgument := ReplyTo (Option EngineID) (Option MailboxID);

ReplyTo

ReplyTo (Option EngineID) (Option MailboxID)

This matchable argument contains the address and mailbox ID of where the response message should be sent.

Precomputation results

The Reads For Engine does not require any non-trivial pre-computations.

syntax alias ReadsForPrecomputation := Unit;

Guards

Auxiliary Juvix code

Type alias for the guard.

ReadsForGuard : Type :=
Guard
ReadsForLocalState
ReadsForMailboxState
ReadsForTimerHandle
ReadsForMatchableArgument
ReadsForActionLabel
ReadsForPrecomputation;

ReadsForGuardOutput : Type :=
GuardOutput
ReadsForMatchableArgument
ReadsForActionLabel
ReadsForPrecomputation;

readsForQueryGuard

flowchart TD
    C{ReadsForRequest<br>received?}
    C -->|Yes| D[enabled]
    C -->|No| E[not enabled]
    D --> F([DoReadsForQuery])
readsForQueryGuard flowchart
readsForQueryGuard
(t : TimestampedTrigger ReadsForTimerHandle)
(env : ReadsForEnvironment)
: Option ReadsForGuardOutput :=
case getMessageFromTimestampedTrigger t of
| some (MsgReadsFor (ReadsForRequest x y)) :=
do {
sender <- getSenderFromTimestampedTrigger t;
pure
mkGuardOutput@{
matchedArgs := [ReplyTo (some sender) none];
actionLabel := DoReadsForQuery x y;
precomputationTasks := unit
};
}
| _ := none;

submitEvidenceGuard

flowchart TD
    C{SubmitReadsForEvidence<br>Request received?}
    C -->|Yes| D[enabled]
    C -->|No| E[not enabled]
    D --> F([DoSubmitEvidence])
submitEvidenceGuard flowchart
submitEvidenceGuard
(t : TimestampedTrigger ReadsForTimerHandle)
(env : ReadsForEnvironment)
: Option ReadsForGuardOutput :=
case getMessageFromTimestampedTrigger t of
| some (MsgReadsFor (SubmitReadsForEvidenceRequest x)) :=
do {
sender <- getSenderFromTimestampedTrigger t;
pure
mkGuardOutput@{
matchedArgs := [ReplyTo (some sender) none];
actionLabel := DoSubmitEvidence x;
precomputationTasks := unit
};
}
| _ := none;

queryEvidenceGuard

flowchart TD
    C{QueryReadsForEvidence<br>Request received?}
    C -->|Yes| D[enabled]
    C -->|No| E[not enabled]
    D --> F([DoQueryEvidence])
queryEvidenceGuard flowchart
queryEvidenceGuard
(t : TimestampedTrigger ReadsForTimerHandle)
(env : ReadsForEnvironment)
: Option ReadsForGuardOutput :=
case getMessageFromTimestampedTrigger t of
| some (MsgReadsFor (QueryReadsForEvidenceRequest x)) :=
do {
sender <- getSenderFromTimestampedTrigger t;
pure
mkGuardOutput@{
matchedArgs := [ReplyTo (some sender) none];
actionLabel := DoQueryEvidence x;
precomputationTasks := unit
};
}
| _ := none;

Action function

Auxiliary Juvix code

Type alias for the action function.

ReadsForActionInput : Type :=
ActionInput
ReadsForLocalState
ReadsForMailboxState
ReadsForTimerHandle
ReadsForMatchableArgument
ReadsForActionLabel
ReadsForPrecomputation;

ReadsForActionEffect : Type :=
ActionEffect
ReadsForLocalState
ReadsForMailboxState
ReadsForTimerHandle
ReadsForMatchableArgument
ReadsForActionLabel
ReadsForPrecomputation;

readsForAction (input : ReadsForActionInput) : ReadsForActionEffect :=
let
env := ActionInput.env input;
out := ActionInput.guardOutput input;
localState := EngineEnvironment.localState env;
in case GuardOutput.actionLabel out of
| DoReadsForQuery externalIdentityA externalIdentityB :=
case GuardOutput.matchedArgs out of {
| ReplyTo (some whoAsked) _ :: _ :=
let
hasEvidence :=
elem
\ {a b := a && b}
true
(map
\ {evidence :=
isEQ
(Ord.cmp
(ReadsForEvidence.fromIdentity evidence)
externalIdentityA)
&& isEQ
(Ord.cmp
(ReadsForEvidence.toIdentity evidence)
externalIdentityB)}
(toList (ReadsForLocalState.evidenceStore localState)));
responseMsg :=
ReadsForResponse@{
readsFor := hasEvidence;
err := none
};
in mkActionEffect@{
newEnv := env;
producedMessages :=
[ mkEngineMessage@{
sender := mkPair none (some (EngineEnvironment.name env));
target := whoAsked;
mailbox := some 0;
msg := MsgReadsFor responseMsg
}
];
timers := [];
spawnedEngines := []
}
| _ :=
mkActionEffect@{
newEnv := env;
producedMessages := [];
timers := [];
spawnedEngines := []
}
}
| DoSubmitEvidence evidence :=
case GuardOutput.matchedArgs out of {
| ReplyTo (some whoAsked) _ :: _ :=
let
isValid := ReadsForLocalState.verifyEvidence localState evidence;
in case isValid of {
| true :=
let
alreadyExists :=
elem
\ {a b := a && b}
true
(map
\ {e := isEQ (Ord.cmp e evidence)}
(toList
(ReadsForLocalState.evidenceStore localState)));
in case alreadyExists of {
| true :=
let
responseMsg :=
SubmitReadsForEvidenceResponse@{
err := some "Evidence already exists."
};
in mkActionEffect@{
newEnv := env;
producedMessages :=
[ mkEngineMessage@{
sender :=
mkPair
none
(some (EngineEnvironment.name env));
target := whoAsked;
mailbox := some 0;
msg := MsgReadsFor responseMsg
}
];
timers := [];
spawnedEngines := []
}
| false :=
let
newEvidenceStore :=
Set.insert
evidence
(ReadsForLocalState.evidenceStore localState);
updatedLocalState :=
localState@ReadsForLocalState{evidenceStore := newEvidenceStore};
newEnv' :=
env@EngineEnvironment{localState := updatedLocalState};
responseMsg :=
SubmitReadsForEvidenceResponse@{
err := none
};
in mkActionEffect@{
newEnv := newEnv';
producedMessages :=
[ mkEngineMessage@{
sender :=
mkPair
none
(some (EngineEnvironment.name env));
target := whoAsked;
mailbox := some 0;
msg := MsgReadsFor responseMsg
}
];
timers := [];
spawnedEngines := []
}
}
| false :=
let
responseMsg :=
SubmitReadsForEvidenceResponse@{
err := some "Invalid evidence provided."
};
in mkActionEffect@{
newEnv := env;
producedMessages :=
[ mkEngineMessage@{
sender :=
mkPair none (some (EngineEnvironment.name env));
target := whoAsked;
mailbox := some 0;
msg := MsgReadsFor responseMsg
}
];
timers := [];
spawnedEngines := []
}
}
| _ :=
mkActionEffect@{
newEnv := env;
producedMessages := [];
timers := [];
spawnedEngines := []
}
}
| DoQueryEvidence externalIdentity' :=
case GuardOutput.matchedArgs out of
| ReplyTo (some whoAsked) _ :: _ :=
let
relevantEvidence :=
AVLfilter
\ {evidence :=
isEQ
(Ord.cmp
(ReadsForEvidence.fromIdentity evidence)
externalIdentity')
|| isEQ
(Ord.cmp
(ReadsForEvidence.toIdentity evidence)
externalIdentity')}
(ReadsForLocalState.evidenceStore localState);
responseMsg :=
QueryReadsForEvidenceResponse@{
externalIdentity := externalIdentity';
evidence := relevantEvidence;
err := none
};
in mkActionEffect@{
newEnv := env;
producedMessages :=
[ mkEngineMessage@{
sender := mkPair none (some (EngineEnvironment.name env));
target := whoAsked;
mailbox := some 0;
msg := MsgReadsFor responseMsg
}
];
timers := [];
spawnedEngines := []
}
| _ :=
mkActionEffect@{
newEnv := env;
producedMessages := [];
timers := [];
spawnedEngines := []
};

Conflict solver

readsForConflictSolver
: Set ReadsForMatchableArgument -> List (Set ReadsForMatchableArgument)
| _ := [];

ReadsForBehaviour type

ReadsForBehaviour : Type :=
EngineBehaviour
ReadsForLocalState
ReadsForMailboxState
ReadsForTimerHandle
ReadsForMatchableArgument
ReadsForActionLabel
ReadsForPrecomputation;

ReadsForBehaviour instance

readsForBehaviour : ReadsForBehaviour :=
mkEngineBehaviour@{
guards := [readsForQueryGuard; submitEvidenceGuard; queryEvidenceGuard];
action := readsForAction;
conflictSolver := readsForConflictSolver
};