raw
ffa_ch2_logicals.kv     1 with Words; use Words;
ffa_ch2_logicals.kv     2 with FZ_Type; use FZ_Type;
ffa_ch2_logicals.kv     3 
ffa_ch2_logicals.kv     4 
ffa_ch2_logicals.kv     5 package FZ_Basic is
ffa_ch2_logicals.kv     6    
ffa_ch2_logicals.kv     7    pragma Pure;
ffa_ch2_logicals.kv     8    
ffa_ch2_logicals.kv     9    -- N := 0
ffa_ch2_logicals.kv    10    procedure FZ_Clear(N : out FZ);
ffa_ch2_logicals.kv    11    
ffa_ch2_logicals.kv    12    -- First word of N := Source
ffa_ch2_logicals.kv    13    procedure FZ_Set_Head(N : out FZ; Source : in Word);
ffa_ch2_logicals.kv    14    
ffa_ch2_logicals.kv    15    -- First word of N
ffa_ch2_logicals.kv    16    function FZ_Get_Head(N : in FZ) return Word;
ffa_ch2_logicals.kv    17    
ffa_ch2_logicals.kv    18    -- Exchange X and Y
ffa_ch2_logicals.kv    19    procedure FZ_Swap(X : in out FZ; Y : in out FZ);
ffa_ch2_logicals.kv    20    pragma Precondition(X'Length = Y'Length);
ffa_ch2_logicals.kv    21    
ffa_ch2_logicals.kv    22    -- Constant-time MUX: Sel = 0: Result := X; Sel = 1: Result := Y
ffa_ch2_logicals.kv    23    procedure FZ_Mux(X : in FZ; Y : in FZ; Result : out FZ; Sel : in WBool);
ffa_ch2_logicals.kv    24    pragma Precondition(X'Length = Y'Length and X'Length = Result'Length);
ffa_ch2_logicals.kv    25    
ffa_ch2_logicals.kv    26 end FZ_Basic;