← All compilation units

Flyology.Process_Generations.Protocol

Description

One wire byte.

Decode

procedure Decode (Input : Octet_Array; Item : out Frame; Status : out Decode_Status)

Decode one complete frame. Need_More_Data reports an incomplete header or payload; Wrong_Length reports bytes after one complete frame. Item is initialized to a harmless value on every non-Decoded outcome.

Parameters
Input

Candidate complete-frame bytes

Item

Decoded frame, or a harmless initialized value on failure

Status

Decode classification

Decode_Status

type Decode_Status is
  (Decoded,
   Need_More_Data,
   Wrong_Length,
   Bad_Magic,
   Unsupported_Version,
   Unknown_Message,
   Invalid_Identity,
   Invalid_Sequence,
   Oversized_Payload,
   Nonzero_Reserved);

Fail-closed decode classification.

Enumeration literals
Decoded

Frame or header is structurally valid

Need_More_Data

Input ends before the declared frame extent

Wrong_Length

Input contains bytes beyond one complete frame

Bad_Magic

Header does not carry the Flyology protocol marker

Unsupported_Version

Header protocol version is unsupported

Unknown_Message

Message kind code is unknown

Invalid_Identity

An authority component is zero

Invalid_Sequence

Direction sequence is zero

Oversized_Payload

Declared payload exceeds the bounded maximum

Nonzero_Reserved

Reserved header bytes are not zero

Encode

procedure Encode (Item : Frame; Output : out Octet_Array)

Encode one frame into an exact-sized caller buffer.

Parameters
Item

Frame to encode

Output

Exact-sized destination bytes

Encoded_Length

function Encoded_Length (Item : Frame) return Positive

Return the exact wire extent for Item.

Parameters
Item

Decoded frame

Return value

Header and significant payload size in bytes

Frame

type Frame is record
   Kind      : Message_Kind;
   Authority : Upgrade_Handle;
   Sequence  : Interfaces.Unsigned_64;
   Length    : Payload_Length;
   Payload   : Payload_Buffer;
end record;

One decoded control message. Only Payload (0 .. Length - 1) is significant. Decode zeroes the unused suffix.

Record fields
Kind

Message operation

Authority

Exact upgrade transaction

Sequence

Nonzero monotonically increasing direction sequence

Length

Significant payload bytes

Payload

Fixed bounded payload storage

Header_Length

Header_Length    : constant Positive := 48;

Fixed wire-header size in bytes.

Inspect_Header

procedure Inspect_Header (Input : Octet_Array; Length : out Payload_Length; Status : out Decode_Status)

Validate one exact header and return its declared payload size. Decoded means the header is structurally valid even when a payload must still be read. Wrong_Length means Input is not exactly Header_Length bytes.

Parameters
Input

Candidate header bytes

Length

Declared payload length, or zero on failure

Status

Header classification

Maximum_Frame

Maximum_Frame    : constant Positive := Header_Length + Maximum_Payload;

Largest complete frame in bytes.

Maximum_Payload

Maximum_Payload  : constant Natural := 2_048;

Largest permitted control payload in bytes.

Message_Kind

type Message_Kind is
  (Hello,
   Provision,
   Expect_Capability,
   Capability_Ready,
   Capability_Adopted,
   Prepared_Message,
   Activate,
   Ready_Message,
   …,
   Acknowledgment);

Control-plane message kind. Capability descriptors travel on the separate ancillary-data lane only after the matching expectation.

Enumeration literals
Hello

Candidate authentication greeting

Provision

Desired topology and role

Expect_Capability

Permission to receive the next capability

Capability_Ready

Sender-side capability readiness

Capability_Adopted

Receiver-side capability adoption

Prepared_Message

Candidate preparation completed

Activate

Start the candidate server

Ready_Message

Candidate readiness and topology proof

Start_Canary_Message

Grant canary admission

Cancel_Message

Begin candidate cancellation

Admission_Revoked_Message

New admission is disabled

Drained_Message

Managed work is quiescent

Compensation_Message

Application compensation outcome

Promote_Message

Promote the candidate

Drain_Message

Drain a previous or retiring image

Commit_Message

Commit promotion bookkeeping

Failure_Message

Bounded peer failure description

Shutdown_Message

Stop and drain the image

Acknowledgment

Successful completion of the requested boundary

Octet

subtype Octet is Interfaces.Unsigned_8;

One wire byte.

Octet_Array

type Octet_Array is array (Wire_Index range <>) of Octet;

Contiguous wire bytes with caller-selected bounds.

Payload_Buffer

type Payload_Buffer is array (Payload_Index) of Octet;

Fixed storage for one bounded control payload.

Payload_Index

subtype Payload_Index is Natural range 0 .. Maximum_Payload - 1;

Index range of fixed payload storage.

Payload_Length

subtype Payload_Length is Natural range 0 .. Maximum_Payload;

Significant control-payload length.

Protocol_Version

Protocol_Version : constant Interfaces.Unsigned_16 := 1;

Current control-frame protocol version.

Wire_Count

subtype Wire_Count is Natural range 0 .. Maximum_Frame;

Count range for one complete frame buffer.

Wire_Index

subtype Wire_Index is Natural range 0 .. Maximum_Frame - 1;

Index range for one complete frame buffer.