I have a File_Reader composed of two records, File and Buffer. I would like to ensure both Records always have a valid buffer size when initialized, i.e. Data_File.IO_Buffer_Size is equal to Data_In.Size.

I couldn't find a way of initializing a record component's value with another record's component value or discriminant, so I figured I would at least apply a static predicate which was unsuccessful. Using dynamic predicate as,an alternative poses issues in a LightRuntime environment.

I could easily add a Buffer_Size discriminant to File_Reader, but I would like to explore alternative solutions. Lastly, the record layouts must be preserved since they are memory mapped using representation clauses which are not shown:

type File is 
   record
      Name           : String;
      IO_Buffer_Size : Buffer_Size;
   end record; 

type Buffer(Size : Buffer_Size := 300)  is         
   record
      Pos   : Buffer_Size := 0;
      Value : String(1 .. Size);
   end record;

type File_Reader(Name : String) is 
   record        
       Data_In      : Buffer;    
       Data_File    : File := (Name, Data_In.Size); -- Won't work
   end record;