(256 . 6)(256 . 14)
118 XY_Lo'Length = XY_Hi'Length and
119 XY_Lo'Length = ((X'Length + Y'Length) / 2);
120
121 -- Square. Preserves the inputs.
122 procedure FFA_FZ_Square(X : in FZ;
123 XX_Lo : out FZ;
124 XX_Hi : out FZ)
125 with Pre => XX_Lo'Length = X'Length and
126 XX_Hi'Length = X'Length and
127 X'Length mod 2 = 0;
128
129 ----------------------------------------------------------------------------
130 --- Modular Operations on FZ
131 ----------------------------------------------------------------------------