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
  | MsgReadsForResponse ResponseReadsFor
  | MsgSubmitReadsForEvidenceRequest RequestSubmitReadsForEvidence
  | MsgSubmitReadsForEvidenceResponse ResponseSubmitReadsForEvidence
  | MsgQueryReadsForEvidenceRequest RequestQueryReadsForEvidence
  | MsgQueryReadsForEvidenceResponse ResponseQueryReadsForEvidence;

Message sequence diagrams

Submitting reads_for evidence

sequenceDiagram
    participant Client
    participant ReadsForEngine

    Client->>ReadsForEngine: RequestSubmitReadsForEvidence
    Note over ReadsForEngine: Verify and store evidence
    ReadsForEngine->>Client: ResponseSubmitReadsForEvidence
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: ResponseReadsFor
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: ResponseQueryReadsForEvidence
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.

ResponseReadsFor

type ResponseReadsFor :=
  mkResponseReadsFor@{
    readsFor : Bool;
    err : Option String;
  };

Response 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.

ResponseSubmitReadsForEvidence

type ResponseSubmitReadsForEvidence :=
  mkResponseSubmitReadsForEvidence@{
    err : Option String;
  };

Response 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.

ResponseQueryReadsForEvidence

type ResponseQueryReadsForEvidence :=
  mkResponseQueryReadsForEvidence@{
    externalIdentity : ExternalIdentity;
    evidence : Set ReadsForEvidence;
    err : Option String;
  };

Response 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
  | MsgReadsForResponse ResponseReadsFor
  | MsgSubmitReadsForEvidenceRequest RequestSubmitReadsForEvidence
  | MsgSubmitReadsForEvidenceResponse ResponseSubmitReadsForEvidence
  | MsgQueryReadsForEvidenceRequest RequestQueryReadsForEvidence
  | MsgQueryReadsForEvidenceResponse ResponseQueryReadsForEvidence;

Engine Components