Package: LSC.Pad32

Dependencies

with LSC.Types;
use type LSC.Types.Word32;
use type LSC.Types.Word64;
use type LSC.Types.Index;
 inherit
    LSC.Types,
    LSC.Byteorder32;

Description

Cryptographic padding for arrays of 32-bit words

Header

package LSC.Pad32
is
 

Other Items:

procedure Block_Terminate
  (Block  : in out Types.Word32_Array_Type;
   Length : in     Types.Word64);
Terminate a Word32 array

The array Block is terminated by setting the bit at (Length + 1) to 1 and all following bits to 0.

NOTE: The postcondition currently does not completely express the intended behaviour of the operation!
 derives Block from *,
                    Length;
 pre
    Types.Index'First + Types.Index (Length / 32) in Block'Range;
 post
    (for all I in Types.Index range
        Types.Index'First + Types.Index (Length / 32) + 1 .. Block'Last => (Block (I) = 0));
end LSC.Pad32;