(17 . 7)(17 . 7)
1274 ------------------------------------------------------------------------------
1275 ------------------------------------------------------------------------------
1276
1277 with Words; use Words;
1278 with Words; use Words;
1279 with FZ_Type; use FZ_Type;
1280
1281
(27 . 25)(27 . 30)
1283
1284 -- Determine the Bitness of N
1285 function FZ_Bitness(N : in FZ) return Bit_Count;
1286 pragma Inline_Always(FZ_Bitness);
1287
1288 -- N := 0
1289 procedure FZ_Clear(N : out FZ);
1290 pragma Inline_Always(FZ_Clear);
1291
1292 -- Set given FZ to a given truth value
1293 procedure WBool_To_FZ(V : in WBool; N : out FZ);
1294 pragma Inline_Always(WBool_To_FZ);
1295
1296 -- First word of N := Source
1297 procedure FZ_Set_Head(N : out FZ; Source : in Word);
1298 pragma Inline_Always(FZ_Set_Head);
1299
1300 -- First word of N
1301 function FZ_Get_Head(N : in FZ) return Word;
1302 pragma Inline_Always(FZ_Get_Head);
1303
1304 -- Exchange X and Y
1305 procedure FZ_Swap(X : in out FZ; Y : in out FZ);
1306 pragma Precondition(X'Length = Y'Length);
1307 pragma Inline_Always(FZ_Swap);
1308
1309 -- Constant-time MUX: Sel = 0: Result := X; Sel = 1: Result := Y
1310 procedure FZ_Mux(X : in FZ; Y : in FZ; Result : out FZ; Sel : in WBool);
1311 pragma Precondition(X'Length = Y'Length and X'Length = Result'Length);
1312 pragma Inline_Always(FZ_Mux);
1313
1314 end FZ_Basic;