ipv6.rflx

with Protocol_Numbers;

package IPv6 is

   -- Types

   -- The value [...] MUST be ignored by the receiver
   -- https://github.com/Componolit/RecordFlux/issues/601
   type Reserved_2 is range 0 .. 0 with Size => 2;
   type Reserved_8 is range 0 .. 0 with Size => 8;
   type Reserved_15 is range 0 .. 0 with Size => 15;
   type Reserved_20 is range 0 .. 0 with Size => 20;
   type Reserved_32 is range 0 .. 0 with Size => 32;

   -- IPv6 address (RFC 4291, 2.5)

   type Address is
      message
         null
            then Data
               with Size => 128;
         Data : Opaque;
      end message;

   type Addresses is sequence of Address;

   -- Options (RFC 8200, 4.2)

   type Option_Action is
      (Skip                                        => 0,
       Discard                                     => 1,
       Discard_With_Parameter_Problem              => 2,
       Discard_With_Parameter_Problem_If_Multicast => 3)
   with Size => 2;

   type Option_Value is
      (Pad1         => 0,
       PadN         => 1,
       Router_Alert => 5)
   with Size => 5;

   type Option_Type is
      message
         Action : Option_Action;
         May_Change : Boolean;
         Value : Option_Value;
      end message;

   type Data_Len is range 0 .. 2 ** 8 - 1 with Size => 8;

   type Option is
      message
         Option_Type : Option_Type
            then null
               if Option_Type_Action = Skip
                  and Option_Type_May_Change = False
                  and Option_Type_Value = Pad1
            then Opt_Data_Len
               if Option_Type_Action /= Skip
                  or Option_Type_May_Change = True
                  or Option_Type_Value /= Pad1;
         Opt_Data_Len : Data_Len
            then Option_Data
               with Size => 8 * Opt_Data_Len;
         Option_Data : Opaque;
      end message;

   type Options is sequence of Option;

   type Options_Base_Header is
      message
         Next_Header : Protocol_Numbers::Assigned_Internet_Protocol_Numbers;
         Hdr_Ext_Len : Data_Len;
         Options : Options
            -- RFC 8200, 4.3:
            -- Hdr Ext Len: Length of the [...] Options header in 8-octet units not including
            -- the first 8 octets.
            -- As the length field contains the *total* length of the options header minus 8
            -- octets, we need to add 8 octets (64 bit) to the length, but subtract Hdr_Ext_Len
            -- and Next_Header to get the size of the Options.
            with Size => 64 - Hdr_Ext_Len'Size - Next_Header'Size + 64 * Hdr_Ext_Len;
         Data : Opaque
            -- https://github.com/Componolit/RecordFlux-specifications/issues/101
            with Size => Message'Last - Options'Last;
      end message;

   -- Hop-by-Hop Options Header (RFC 8200, 4.3)

   type Hop_By_Hop_Options_Header is new Options_Base_Header;

   -- Routing Header (RFC 8200, 4.4)

   -- Routing types
   -- https://www.iana.org/assignments/ipv6-parameters/ipv6-parameters-3.csv
   type Routing_Type is
      (RT_Type_2           => 2,
       RT_RPL_Source_Route => 3,
       RT_Segment_Routing  => 4,
       RT_Experiment_1     => 253,
       RT_Experiment_2     => 254,
       RT_Reserved         => 255)
   with Size => 8, Always_Valid;

   type Segments_Count is range 0 .. 2 ** 8 - 1 with Size => 8;

   type Routing_Base_Header is
      message
         Hdr_Ext_Len : Data_Len;
         Routing_Type : Routing_Type;
         Data : Opaque
            -- RFC 8200, 4.4: 8-bit unsigned integer. Length of the Routing header in 8-octet
            -- units, not including the first 8 octets.
            -- We need to add 8 octets (64 bit) to the length, but subtract Routing_Type,
            -- Hdr_Ext_Len and also Next_Header_Field (8 bits) which is contained in the outer
            -- Routing_Header.
            with Size => 64 - Routing_Type'Size - Hdr_Ext_Len'Size - 8 + 64 * Hdr_Ext_Len;
      end message;

   -- Type 2 routing header (RFC 6275, 6.4)
   type Routing_Header_Type_2 is
      message
         Segments_Left : Segments_Count
            if Segments_Left = 1;
         Reserved : Reserved_32;
         Home_Address : Address;
      end message;

   for Routing_Base_Header use (Data => Routing_Header_Type_2)
      if Hdr_Ext_Len = 2 and Routing_Type = RT_Type_2;

   -- RPL Routing Header (RFC 6554, 3)

   type Cmpr_Length is range 0 .. 15 with Size => 4;
   type Pad_Length is range 0 .. 15 with Size => 4;

   -- https://github.com/Componolit/RecordFlux/issues/608
   -- As per RFC 6554, section 3, the segments sent in the RPL routing header actually are a
   -- vector of addresses. However, these are not fixed-size IPv6 addresses, but they are
   -- truncated depending on the values of CmprI and CmprE. We cannot specify this as a normal
   -- sequence because those require a static element type.
   type RPL_Routing_Header is
      message
         Segments_Left : Segments_Count;
         CmprI : Cmpr_Length;
         CmprE : Cmpr_Length;
         Pad : Pad_Length;
         Reserved : Reserved_20
            then Padding
               with Size => 8 * Pad
               if Segments_Left = 0
            then Last_Segment
               with Size => 8 * (16 - CmprE)
               if Segments_Left = 1
            then Segments
               with Size => Segments_Left * 8 * (16 - CmprI)
               if Segments_Left > 1;
         Segments : Opaque
            then Last_Segment
               with Size => 8 * (16 - CmprE);
         Last_Segment : Opaque
            then Padding
               with Size => 8 * Pad;
         Padding : Opaque;
      end message;

   for Routing_Base_Header use (Data => RPL_Routing_Header)
      if Routing_Type = RT_RPL_Source_Route;

   -- Segment Routing Header, SRH (RFC 8754, 2)

   type SRH_Last_Entry_Index is range 0 .. 2 ** 8 - 1 with Size => 8;
   type SRH_Tag is range 0 .. 2 ** 16 - 1 with Size => 16;

   type SRH_TLV_Kind is
      (SRH_TK_Pad1         =>   0,
       SRH_TK_Reserved_1   =>   1,
       SRH_TK_Reserved_2   =>   2,
       SRH_TK_Reserved_3   =>   3,
       SRH_TK_PadN         =>   4,
       SRH_TK_HMAC         =>   5,
       SRH_TK_Reserved_6   =>   6,
       SRH_TK_EuT_124      => 124,
       SRH_TK_EuT_125      => 125,
       SRH_TK_EuT_126      => 126,
       SRH_TK_EuT_252      => 252,
       SRH_TK_EuT_253      => 253,
       SRH_TK_EuT_254      => 254,
       SRH_TK_Reserved_255 => 255)
   with Size => 8, Always_Valid;

   type SRH_TLV is
      message
         Kind : SRH_TLV_Kind
            then null
               if Kind = SRH_TK_Pad1
            then Length
               if Kind /= SRH_TK_Pad1;
         Length : Data_Len;
         Data : Opaque
            with Size => 8 * Length;
      end message;

   type SRH_HMAC_Key_ID is mod 2 ** 32;

   type SRH_HMAC_TLV is
      message
         Dest_Addr_Verification_Disable : Boolean;
         Reserved : Reserved_15;
         HMAC_Key_ID : SRH_HMAC_Key_ID;
         HMAC : Opaque
            -- https://github.com/Componolit/RecordFlux-specifications/issues/101
            with Size => Message'Last - HMAC_Key_ID'Last;
      end message;

   for SRH_TLV use (Data => SRH_HMAC_TLV)
      if Kind = SRH_TK_HMAC;

   type Segment_Routing_Header is
      message
         Segments_Left : Segments_Count;
         Last_Entry : SRH_Last_Entry_Index;
         Flags : Reserved_8;
         Tag : SRH_Tag;
         Segments : Addresses
            -- Last Entry contains the index (zero based), in the Segment List, of the last
            -- element of the Segment List.
            -- https://github.com/Componolit/RecordFlux/issues/404
            -- with Size => Address'Size * (Last_Entry + 1);
            with Size => 128 * (Last_Entry + 1);
      end message;

   for Routing_Base_Header use (Data => Segment_Routing_Header)
      if Routing_Type = RT_Segment_Routing;

   type Routing_Header is
      message
         Next_Header : Protocol_Numbers::Assigned_Internet_Protocol_Numbers;
         RH : Routing_Base_Header;
         Data : Opaque
            -- https://github.com/Componolit/RecordFlux-specifications/issues/101
            with Size => 128;
      end message;

   -- Fragment Header (RFC 8200, 4.5)

   type FH_Offset is range 0 .. 2 ** 13 - 1 with Size => 13;
   type FH_Identification is mod 2 ** 32;

   type Fragment_Header is
      message
         Next_Header : Protocol_Numbers::Assigned_Internet_Protocol_Numbers;
         Reserved_1 : Reserved_8;
         Fragment_Offset : FH_Offset;
         Reserved_2 : Reserved_2;
         More_Fragments : Boolean;
         Identification : FH_Identification;
         Data : Opaque
            -- https://github.com/Componolit/RecordFlux-specifications/issues/101
            with Size => Message'Last - Identification'Last;
      end message;

   -- Destination Options Header (RFC 8200, 4.6)

   type Destination_Options_Header is new Options_Base_Header;

   -- Packet (RFC 8200, 3)

   type Version is range 6 .. 6 with Size => 4;
   type Traffic_Class is mod 2 ** 8;
   type Flow_Label is mod 2 ** 20;
   type Payload_Length is range 0 .. 2 ** 16 - 1 with Size => 16;
   type Hop_Limit is range 0 .. 2 ** 8 - 1 with Size => 8;

   type Packet is
      message
         Version : Version;
         Traffic_Class : Traffic_Class;
         Flow_Label : Flow_Label;
         Payload_Length : Payload_Length;
         Next_Header : Protocol_Numbers::Assigned_Internet_Protocol_Numbers;
         Hop_Limit : Hop_Limit;
         Source : Address;
         Destination : Address
            then Payload
               with Size => 8 * Payload_Length;
         Payload : Opaque;
      end message;

   -- Router Alert Option (RFC 2711, 2.1)

   type Router_Alert_Option_Value is
      (RAO_Multicast_Listener_Discover => 0,
       RAO_RSVP                        => 1,
       RAO_Active_Networks             => 2)
   with Size => 16;

   type Router_Alert_Option is
      message
         Value : Router_Alert_Option_Value;
      end message;

   for Option use (Option_Data => Router_Alert_Option)
      if Option_Type_Action = Skip
         and Option_Type_May_Change = False
         and Option_Type_Value = Router_Alert;

   -- Null Header (RFC 8200, 4.7)
   type Null_Header is null message;

   -----------------------------
   -- Next header refinements --
   -----------------------------

   -- Hop-by-Hop Options Header
   for Hop_By_Hop_Options_Header use (Data => Hop_By_Hop_Options_Header)
      if Next_Header = Protocol_Numbers::HOPOPT;

   for Hop_By_Hop_Options_Header use (Data => Routing_Header)
      if Next_Header = Protocol_Numbers::IPv6_Route;

   for Hop_By_Hop_Options_Header use (Data => Fragment_Header)
      if Next_Header = Protocol_Numbers::IPv6_Frag;

   for Hop_By_Hop_Options_Header use (Data => Null_Header)
      if Next_Header = Protocol_Numbers::IPv6_NoNxt;

   for Hop_By_Hop_Options_Header use (Data => Destination_Options_Header)
      if Next_Header = Protocol_Numbers::IPv6_Opts;

   for Hop_By_Hop_Options_Header use (Data => Packet)
      if Next_Header = Protocol_Numbers::IPv6;

   -- Routing header
   for Routing_Header use (Data => Hop_By_Hop_Options_Header)
      if Next_Header = Protocol_Numbers::HOPOPT;

   for Routing_Header use (Data => Routing_Header)
      if Next_Header = Protocol_Numbers::IPv6_Route;

   for Routing_Header use (Data => Fragment_Header)
      if Next_Header = Protocol_Numbers::IPv6_Frag;

   for Routing_Header use (Data => Null_Header)
      if Next_Header = Protocol_Numbers::IPv6_NoNxt;

   for Routing_Header use (Data => Destination_Options_Header)
      if Next_Header = Protocol_Numbers::IPv6_Opts;

   for Routing_Header use (Data => Packet)
      if Next_Header = Protocol_Numbers::IPv6;

   -- Fragment Header
   for Fragment_Header use (Data => Hop_By_Hop_Options_Header)
      if Next_Header = Protocol_Numbers::HOPOPT;

   for Fragment_Header use (Data => Routing_Header)
      if Next_Header = Protocol_Numbers::IPv6_Route;

   for Fragment_Header use (Data => Fragment_Header)
      if Next_Header = Protocol_Numbers::IPv6_Frag;

   for Fragment_Header use (Data => Null_Header)
      if Next_Header = Protocol_Numbers::IPv6_NoNxt;

   for Fragment_Header use (Data => Destination_Options_Header)
      if Next_Header = Protocol_Numbers::IPv6_Opts;

   for Fragment_Header use (Data => Packet)
      if Next_Header = Protocol_Numbers::IPv6;

   -- Destination Options Header
   for Destination_Options_Header use (Data => Hop_By_Hop_Options_Header)
      if Next_Header = Protocol_Numbers::HOPOPT;

   for Destination_Options_Header use (Data => Routing_Header)
      if Next_Header = Protocol_Numbers::IPv6_Route;

   for Destination_Options_Header use (Data => Fragment_Header)
      if Next_Header = Protocol_Numbers::IPv6_Frag;

   for Destination_Options_Header use (Data => Null_Header)
      if Next_Header = Protocol_Numbers::IPv6_NoNxt;

   for Destination_Options_Header use (Data => Destination_Options_Header)
      if Next_Header = Protocol_Numbers::IPv6_Opts;

   for Destination_Options_Header use (Data => Packet)
      if Next_Header = Protocol_Numbers::IPv6;

   -- Packet
   for Packet use (Payload => Hop_By_Hop_Options_Header)
      if Next_Header = Protocol_Numbers::HOPOPT;

   for Packet use (Payload => Routing_Header)
      if Next_Header = Protocol_Numbers::IPv6_Route;

   for Packet use (Payload => Fragment_Header)
      if Next_Header = Protocol_Numbers::IPv6_Frag;

   for Packet use (Payload => Null_Header)
      if Next_Header = Protocol_Numbers::IPv6_NoNxt;

   for Packet use (Payload => Destination_Options_Header)
      if Next_Header = Protocol_Numbers::IPv6_Opts;

   for Packet use (Payload => Packet)
      if Next_Header = Protocol_Numbers::IPv6;

end IPv6;