Skip to content
Juvix imports 

module arch.node.engines.reads_for_messages;

import prelude open;
import arch.node.types.identities open;

ReadsFor Messages

Message interface

type ReadsForMsg :=
  | MsgReadsForRequest RequestReadsFor
  | MsgReadsForReply ReplyReadsFor
  | MsgSubmitReadsForEvidenceRequest RequestSubmitReadsForEvidence
  | MsgSubmitReadsForEvidenceReply ReplySubmitReadsForEvidence
  | MsgQueryReadsForEvidenceRequest RequestQueryReadsForEvidence
  | MsgQueryReadsForEvidenceReply ReplyQueryReadsForEvidence;

Message sequence diagrams

Submitting reads_for evidence

sequenceDiagram
    participant Client
    participant ReadsForEngine

    Client->>ReadsForEngine: RequestSubmitReadsForEvidence
    Note over ReadsForEngine: Verify and store evidence
    ReadsForEngine->>Client: ReplySubmitReadsForEvidence
Submitting reads_for evidence

Querying a reads_for relationship

sequenceDiagram
    participant Client
    participant ReadsForEngine

    Client->>ReadsForEngine: RequestReadsFor (A reads for B?)
    Note over ReadsForEngine: Check stored evidence
    ReadsForEngine->>Client: ReplyReadsFor
Querying a reads_for relationship

Querying reads_for evidence

sequenceDiagram
    participant Client
    participant ReadsForEngine

    Client->>ReadsForEngine: RequestQueryReadsForEvidence (for X)
    Note over ReadsForEngine: Retrieve relevant evidence
    ReadsForEngine->>Client: ReplyQueryReadsForEvidence
Querying reads_for evidence for an identity

Message types

RequestReadsFor

type RequestReadsFor :=
  mkRequestReadsFor@{
    externalIdentityA : ExternalIdentity;
    externalIdentityB : ExternalIdentity;
  };

A request to query whether externalIdentityA can read data encrypted to externalIdentityB.

Arguments
externalIdentityA:
The identity doing the reading.
externalIdentityB:
The identity being read for.

ReplyReadsFor

type ReplyReadsFor :=
  mkReplyReadsFor@{
    readsFor : Bool;
    err : Option String;
  };

Reply indicating whether the reads_for relationship exists.

Arguments
readsFor:
True if externalIdentityA can read for externalIdentityB, False otherwise.
err:
An error message if the query failed.

RequestSubmitReadsForEvidence

type RequestSubmitReadsForEvidence :=
  mkRequestSubmitReadsForEvidence@{
    evidence : ReadsForEvidence;
  };

Request to submit evidence of a reads_for relationship.

Arguments
evidence:
The evidence supporting the reads_for relationship.

ReplySubmitReadsForEvidence

type ReplySubmitReadsForEvidence :=
  mkReplySubmitReadsForEvidence@{
    err : Option String;
  };

Reply acknowledging the submission of evidence.

Arguments
err:
An error message if the submission failed.

RequestQueryReadsForEvidence

type RequestQueryReadsForEvidence :=
  mkRequestQueryReadsForEvidence@{
    externalIdentity : ExternalIdentity;
  };

Request to query all reads_for evidence related to an identity.

Arguments
externalIdentity:
The identity for which to retrieve evidence.

ReplyQueryReadsForEvidence

type ReplyQueryReadsForEvidence :=
  mkReplyQueryReadsForEvidence@{
    externalIdentity : ExternalIdentity;
    evidence : Set ReadsForEvidence;
    err : Option String;
  };

Reply providing the requested evidence.

Arguments
externalIdentity:
The identity for which evidence was requested.
evidence:
A set of ReadsForEvidence related to the identity.
err:
An error message if the query failed.

ReadsForMsg

type ReadsForMsg :=
  | MsgReadsForRequest RequestReadsFor
  | MsgReadsForReply ReplyReadsFor
  | MsgSubmitReadsForEvidenceRequest RequestSubmitReadsForEvidence
  | MsgSubmitReadsForEvidenceReply ReplySubmitReadsForEvidence
  | MsgQueryReadsForEvidenceRequest RequestQueryReadsForEvidence
  | MsgQueryReadsForEvidenceReply ReplyQueryReadsForEvidence;

Engine components