|
Administrateur
- Genre :
- Messages : 22324
|
Source de la spécification du paquet SHA1Source Ada : with System; -- For generic constraints
package SHA1 is
pragma Pure;
-- Types common to all item instances
-- ========================================================================
type State_Type is
(Undefined,
Initialized, -- Reached by invokation of `Initialize`.
Running, -- Pending to recieve data until invokation of `Finalize`.
Valid, -- Hash available.
Invalid); -- No hash available, because message was too long.
subtype Digit_Type is Character range '0' .. 'f';
-- Or more precisely, and if your Ada compiler does not complains:
--
-- subtype Digit_Type is Character range '0' .. 'f'
-- with Static_Predicate =>
-- Digit_Type in -- [3.1]
-- '0' .. '9' |
-- 'a' .. 'f';
subtype Text_Index_Type is Positive range 1 .. 40;
subtype Text_Type is String (Text_Index_Type)
with Static_Predicate =>
(for all I in Text_Type'Range =>
Text_Type (I) in Digit_Type);
-- Items
-- ========================================================================
generic
-- Parameterless
package Items is
-- Methods indepent from hashed item types
-- ---------------------------------------------------------------------
procedure Finalize
with
Pre =>
State in Initialized | Running,
Post =>
(if not Overflowed
then State = Valid
else State = Invalid);
procedure Initialize
with Post =>
(State = Initialized) and
(not Overflowed);
function Overflowed return Boolean -- Message is too long
with Pre => State in Initialized | Running | Valid | Invalid;
function State return State_Type;
-- Incrementally hashing elements buffers
-- ---------------------------------------------------------------------
Bit_Base : constant := 2;
generic
type Bit_Count_Type is range <>
type Element_Type is (<>);
type Index_Type is range <>
type Array_Type is array (Index_Type range <>) of Element_Type;
package Streamers is
-- Make formal parameters visible for clients.
subtype Formal_Bit_Count_Type is Bit_Count_Type;
subtype Formal_Element_Type is Element_Type;
subtype Formal_Index_Type is Index_Type;
subtype Formal_Array_Type is Array_Type;
pragma Assert (0 <= Bit_Count_Type'First);
pragma Assert (Bit_Count_Type'First <= System.Word_Size);
pragma Assert
((Element_Type'Pos (Element_Type'Last) -
Element_Type'Pos (Element_Type'First) + 1) =
(Bit_Base ** Bit_Count_Type'Pos (Bit_Count_Type'Last)));
use type Index_Type;
procedure Append
(Item : Element_Type;
Length : Bit_Count_Type := Bit_Count_Type'Last)
with
Pre =>
State in Initialized | Running,
Post =>
(if 0 < Length
then State = Running
else State = State'Old) and
(if Overflowed'Old
then Overflowed);
-- Append a sub‑string of bits of length `Length`.
-- Append the `Length` lower bits of `Item` starting with the
-- highest weighted bit of these lower bits, down to the lowest.
procedure Append
(Item : Array_Type;
First : Index_Type;
Last : Index_Type)
with
Pre =>
State in Initialized | Running and
Item'First <= First and
Last <= Item'Last,
Post =>
(if First <= Last
then State = Running
else State = State'Old) and
(if Overflowed'Old then Overflowed);
end Streamers;
-- Getting hashes as text
-- ---------------------------------------------------------------------
function Text return Text_Type
with
Pre => (State = Valid),
Post =>
(State = Valid) and
(Text'Result = Text'Result);
-- Avoid compiler warning about Post not mentionning Result.
procedure Write (Target : out Text_Type)
with
Pre => (State = Valid),
Post => (State = Valid);
end Items;
end SHA1; Source du corps du paquet SHA1 (une implémentation de référence)Source Ada : pragma Assertion_Policy (Check);
package body SHA1 is
-- Physical constraints
-- ========================================================================
package Constraints is
-- “Physical” constraints expressed as numbers
Bit_Base : constant := 2; -- [2.1]
Text_Base : constant := 16;
Nibble_Bit_Count : constant := 4; -- [3.1]
Word_Bit_Count : constant := 32; -- [Figure 1], [2.1], [3.1]
Length_Bit_Count : constant := 64; -- [Figure 1]
Hash_Bit_Count : constant := 160; -- [Figure 1]
Block_Bit_Count : constant := 512; -- [Figure 1]
Shedule_Element_Count : constant := 80;
end Constraints;
-- Bits
-- ========================================================================
package Bits is
-- A modular type.
Base : constant := Constraints.Bit_Base;
Width : constant := 1;
type Instance is mod Base ** Width;
end Bits;
-- Nibbles
-- ========================================================================
package Nibbles is
-- A modular type.
-- Group of four bits; half of a byte.
Base : constant := Constraints.Bit_Base;
Width : constant := Constraints.Nibble_Bit_Count;
type Instance is mod Base ** Width; -- [3.1]
end Nibbles;
-- Words
-- ========================================================================
package Words is
-- A modular type.
Base : constant := Constraints.Bit_Base;
Width : constant := Constraints.Word_Bit_Count;
type Instance is mod Base ** Width; -- [3.1]
type Bit_Count_Type is range 0 .. Width;
type Offset_Type is range 0 .. Width; -- Offset in bits [2.2.2]
function Offset (Bit_Count : Bit_Count_Type) return Offset_Type
is (Offset_Type (Bit_Count));
function Shl (N : Offset_Type; X : Bits.Instance) return Instance
is (Instance (X) * (Base ** Natural (N))); -- Additional definition
function Shl (N : Offset_Type; X : Instance) return Instance
is (X * (Base ** Natural (N))); -- Additional definition
function Shr (N : Offset_Type; X : Instance) return Instance
is (X / (Base ** Natural (N))); -- [2.2.2], [3.2]
function Rot_L (N : Offset_Type; X : Instance) return Instance
is (Shl (N, X) or Shr (Width - N, X)); -- [2.2.2], [3.2]
function Rot_R (N : Offset_Type; X : Instance) return Instance
is (Rot_L (Width - N, X)); -- [2.2.2], [3.2]
end Words;
-- Widest binary type
-- ========================================================================
package Widest_Binaries is
-- A modular type.
Base : constant := Constraints.Bit_Base;
Width : constant := System.Word_Size;
-- May be tweaked and manually edited on a per-plateform basis. Choose
-- it so that `Base ** Width` is not greater than `Max_Binary_Modulus`
-- and not greater than the biggest universal integer. Compiler bugs may
-- force you to lower the usable value. A safe value, is that of the
-- natural word size on your plateform, that is, 32 on 32 bits machines
-- and 64 on 64 bits machines. A portable value is 32, as Ada's standard
-- ensures a minimum available width of 32 bits.
pragma Assert (Base ** Width <= System.Max_Binary_Modulus);
pragma Assert (Base ** Width <= System.Max_Int);
type Instance is mod Base ** Width;
type Bit_Count_Type is range 0 .. Width;
type Offset_Type is range 0 .. Width; -- Offset in bits
function Offset (Bit_Count : Bit_Count_Type) return Offset_Type
is (Offset_Type (Bit_Count));
function Shl (N : Offset_Type; X : Instance) return Instance
is (X * (Base ** Natural (N)));
function Shr (N : Offset_Type; X : Instance) return Instance
is (X / (Base ** Natural (N)));
function Rot_L (N : Offset_Type; X : Instance) return Instance
is (Shl (N, X) or Shr (Width - N, X));
function Rot_R (N : Offset_Type; X : Instance) return Instance
is (Rot_L (Width - N, X));
end Widest_Binaries;
-- Parsed message blocks
-- ========================================================================
package Message_Blocks is
-- A fixed capacity block of modular type elements.
-- After initialization, it is filled with an append method.
-- Used as the successive inputs of the incremental hash algorithm.
package Elements renames Words;
Bit_Count : constant := Constraints.Block_Bit_Count;
Element_Count : constant := Bit_Count / Elements.Width;
pragma Assert ((Bit_Count mod Elements.Width) = 0);
subtype Element_Type is Elements.Instance;
subtype Bit_Type is Bits.Instance;
type Instance is private; -- {1}
type Index_Type is range 0 .. Element_Count - 1; -- {2}
type Bit_Count_Type is range 0 .. Bit_Count;
-- 1. There cannot be a public view of an array type. It is written into
-- as an array of bits, and read from as an array of words whose
-- size is defined by the specification. Thus, it is made a private
-- type and is given a public interface with write and read
-- operation using their proper item types.
-- 2. [2.2.1], [2.2.1] and [6.1] for 0 based index
procedure Initialize (Target : out Instance)
with Post => Length (Target) = 0;
function Length (This : Instance) return Bit_Count_Type;
function Is_Full (This : Instance) return Boolean
is (Length (This) = Bit_Count_Type'Last);
function Item
(This : Instance; I : Index_Type)
return Element_Type -- {3}
with Pre => Is_Full (This);
-- 3. [3.1 4 a], [2.2.1] for 0 is left-most byte
procedure Append (Target : in out Instance; Item : Bit_Type)
with
Pre => not Is_Full (Target),
Post => (Length (Target) = Length (Target)'Old + 1);
procedure Append_Zeros
(Target : in out Instance;
Bound : Bit_Count_Type)
with
Pre => Length (Target) <= Bound,
Post => Length (Target) = Bound;
private
type Content_Type is array (Index_Type) of Element_Type;
type Instance is record
M : Content_Type; -- Parsed message part
L : Bit_Count_Type; -- Length occupied
end record;
function Length (This : Instance) return Bit_Count_Type
is (This.L);
function Item (This : Instance; I : Index_Type) return Element_Type
is (This.M (I));
end Message_Blocks;
-- Unparsed (overall) message lengths
-- ========================================================================
package Message_Lengths is
-- A scalar as the overall length of a streamed message while parsed as
-- blocks.
package Blocks renames Message_Blocks;
Bit_Count : constant := Constraints.Length_Bit_Count;
subtype Increment_Type is Blocks.Bit_Count_Type;
use type Increment_Type;
type Instance is private;
-- There cannot be a simple type suitable for a public view. It is
-- updated as a scalar type and needs to be seen as an array of bits
-- to be appended to a message block. Thus it is made a private type
-- with proper methods on proper types provided for each cases.
procedure Initialize (Target : out Instance)
with Post => not Overflowed (Target);
procedure Increment
(Target : in out Instance; Increase : Increment_Type := 1)
with Pre => not Overflowed (Target);
function Overflowed (This : Instance) return Boolean;
procedure Append
(Target : in out Blocks.Instance;
This : in Instance)
with
Pre => Blocks.Length (Target) = Blocks.Bit_Count - Bit_Count,
Post => Blocks.Is_Full (Target);
-- Appends `This` to complete `Target`.
private
-- A polynomial made of the same element type as a parsed message block
-- is; a choice among others, as this was not the only available option
-- to manipulate a minimum of 64 bits width scalar on 32 bits machines.
-- This will work as well on 64 bits machines.
-- After initialization, it is updated with an increment method.
package Elements renames Blocks.Elements;
subtype Element_Type is Elements.Instance;
type Index_Type is range 0 .. (Bit_Count / Elements.Width) - 1;
pragma Assert ((Bit_Count mod Elements.Width) = 0);
type Polynomial_Type is array (Index_Type) of Element_Type;
type Instance is record
P : Polynomial_Type;
Overflowed : Boolean;
end record;
function Overflowed (This : Instance) return Boolean
is (This.Overflowed);
end Message_Lengths;
-- Message hashes
-- ========================================================================
package Hashes is
-- An array of modular type elements.
-- After initialization, it is updated with an external algorithm.
-- Used as the incrementally computed hash of an overall message flow.
package Elements renames Words;
Bit_Count : constant := Constraints.Hash_Bit_Count;
Width : constant := Bit_Count / Elements.Width;
pragma Assert ((Bit_Count mod Elements.Width) = 0);
subtype Element_Type is Elements.Instance;
use type Element_Type;
type Index_Type is range 0 .. Width - 1; -- {1}
type Instance is array (Index_Type) of Element_Type; -- {2}
-- Need not be a private type, and can be exposed as an array,
-- as this is an array per specification and is seen as an array with
-- regards to all operations.
subtype Registers_Type is Instance; -- {3}
-- 1. [2.2.1], [2.2.1] and [5.3.1] for 0 based index
-- 2. [2.2.1], [5.3.1], [2.2.1] for 0 is left-most element
-- 3. [2.2.1], [6.1], [6.1.2]
Initial_Value : constant Instance := -- [5.3.1]
(0 => 16#67452301#,
1 => 16#efcdab89#,
2 => 16#98badcfe#,
3 => 16#10325476#,
4 => 16#c3d2e1f0#);
procedure Initialize (Target : out Instance)
with Post =>
(for all I in Target'Range =>
Target (I) = Initial_Value (I));
-- Algorithm's internal message shedules
-- ---------------------------------------------------------------------
package Message_Shedules is
-- An array of elements of the same type as that of an hash.
-- Used in the hash algorithm (does not persist outside of it).
package Elements renames Hashes.Elements;
Element_Count : constant := Constraints.Shedule_Element_Count;
subtype Element_Type is Elements.Instance;
-- Need not be a private type, and can be exposed as an array,
-- as this is an array per specification and is seen as an array with
-- regards to all operations.
type Index_Type is range 0 .. Element_Count - 1;
type Instance is array (Index_Type) of Element_Type; -- {1}
-- 1. [6.1], [6.1.2]
-- Partition of `Index_Type` range.
subtype Range_1_Type is Index_Type range 0 .. 19;
subtype Range_2_Type is Index_Type range 20 .. 39;
subtype Range_3_Type is Index_Type range 40 .. 59;
subtype Range_4_Type is Index_Type range 60 .. 79;
K_Of_Range_1 : constant Element_Type := 16#5a827999#; -- [4.2.1]
K_Of_Range_2 : constant Element_Type := 16#6ed9eba1#; -- [4.2.1]
K_Of_Range_3 : constant Element_Type := 16#8f1bbcdc#; -- [4.2.1]
K_Of_Range_4 : constant Element_Type := 16#ca62c1d6#; -- [4.2.1]
function K (T : Index_Type) return Element_Type -- [2.2.1], [4.2.1]
is
(case T is
when Range_1_Type => K_Of_Range_1,
when Range_2_Type => K_Of_Range_2,
when Range_3_Type => K_Of_Range_3,
when Range_4_Type => K_Of_Range_4);
end Message_Shedules;
-- Algorithm's functions and incremental method
-- ---------------------------------------------------------------------
package Algorithm is
-- The hash algorithm.
-- Does not defines any type, only a number of functions and a
-- single procedure (an update procedure).
package Blocks renames Message_Blocks;
package Shedules renames Message_Shedules;
subtype Block_Type is Blocks.Instance;
subtype Index_Type is Shedules.Index_Type;
subtype Argument_Type is Hashes.Element_Type;
subtype Result_Type is Hashes.Instance;
use type Argument_Type;
function Ch (X, Y, Z : Argument_Type) return Argument_Type
is ((X and Y) xor ((not X) and Z)); -- [4.1.1]
function Parity (X, Y, Z : Argument_Type) return Argument_Type
is (X xor Y xor Z); -- [4.1.1]
function Maj (X, Y, Z : Argument_Type) return Argument_Type
is ((X and Y) xor (X and Z) xor (Y and Z)); -- [4.1.1]
function F -- [4.1.1]
(T : Index_Type; X, Y, Z : Argument_Type)
return Argument_Type
is
(case T is
when Shedules.Range_1_Type => Ch (X, Y, Z),
when Shedules.Range_2_Type => Parity (X, Y, Z),
when Shedules.Range_3_Type => Maj (X, Y, Z),
when Shedules.Range_4_Type => Parity (X, Y, Z));
procedure Hash -- [6.1.2]
(Target : in out Result_Type; Block : Block_Type)
with Pre => Blocks.Is_Full (Block);
end Algorithm;
-- Texts
-- ---------------------------------------------------------------------
package Texts is
package Base renames Nibbles; -- “Physical” base.
pragma Assert (Base.Instance'Modulus = Constraints.Text_Base);
Digit : constant array (Base.Instance) of Digit_Type :=
('0', '1', '2', '3', '4', '5', '6', '7',
'8', '9', 'a', 'b', 'c', 'd', 'e', 'f');
-- [3.1] Note it's lowercase, not uppercase.
procedure Write (Target : out Text_Type; Item : Instance);
end Texts;
end Hashes;
-- Parsers (turns a message stream into blocks in sequence)
-- ========================================================================
package Parsers is
-- A message block with its incrementally computed hash and length.
-- After initialization, it is updated with an append method.
-- The hash may be retrieved after finalization.
package Blocks renames Message_Blocks;
package Lengths renames Message_Lengths;
subtype State_Type is SHA1.State_Type;
type Instance is private;
function State (This : Instance) return State_Type;
function Overflowed (This : Instance) return Boolean;
function Result (This : Instance) return Hashes.Instance
with Pre => State (This) = Valid;
procedure Initialize (Target : out Instance)
with Post => State (Target) = Initialized;
procedure Append (Target : in out Instance; Item : Bits.Instance)
with
Pre => State (Target) in Initialized | Running,
Post => State (Target) = Running;
procedure Finalize (Target : in out Instance)
with
Pre => State (Target) in Initialized | Running,
Post => State (Target) in Valid | Invalid;
private
type Instance is record
Hash : Hashes.Instance;
Block : Message_Blocks.Instance;
Length : Lengths.Instance;
State : State_Type := Undefined;
end record;
function State (This : Instance) return State_Type
is (This.State);
function Overflowed (This : Instance) return Boolean
is (Lengths.Overflowed (This.Length));
function Result (This : Instance) return Hashes.Instance
is (This.Hash);
end Parsers;
-- Message blocks implementation
-- ========================================================================
package body Message_Blocks is
type Index_Bit_Type is range 0 .. Bit_Count - 1;
procedure Initialize (Target : out Instance)
is begin
Target.L := 0;
end;
pragma Assert
(Index_Bit_Type'Pos (Index_Bit_Type'First) <=
Bit_Count_Type'Pos (Bit_Count_Type'First)); -- H1
pragma Assert
((Bit_Count_Type'Pos (Bit_Count_Type'Last) - 1) <=
Index_Bit_Type'Pos (Index_Bit_Type'Last)); -- H2
pragma Assert (Index_Type'First <= 0); -- H3
pragma Assert
(Index_Bit_Type'Pos (Index_Bit_Type'Last / Elements.Width) <=
Index_Type'Last); -- H4
subtype Offset_Type is Elements.Offset_Type;
use type Offset_Type;
procedure Append (Target : in out Instance; Item : Bit_Type)
is
use type Element_Type;
I : Index_Bit_Type := Index_Bit_Type (Target.L); -- {1}
J : Index_Type := Index_Type (I / Elements.Width); -- {2}
K : Offset_Type :=
Elements.Offset
(Elements.Bit_Count_Type (I mod Elements.Width)); -- {3}
N : Offset_Type := Elements.Width - 1 - K; -- K from left. {4}
M : Content_Type renames Target.M;
-- 1. Valid by H1,H2. As the precondition requires
-- Target.L < Bit_Count_Type'Last, Target.L cannot be more than
-- Bit_Count_Type'Last - 1.
-- 2. Valid by H3,H4
-- 3. Valid by definition (A mod B < B)
-- 4. Valid by K < Elements.Width
begin
if K = 0 then
-- New element to be initialized.
M (J) := Elements.Shl (N => N, X => Item);
else
-- Existing element to be written a bit to.
M (J) := M (J) or Elements.Shl (N => N, X => Item);
end if;
Target.L := Target.L + 1; -- Valid by precondition
end;
procedure Append_Zeros
(Target : in out Instance;
Bound : Bit_Count_Type)
is begin
while Target.L < Bound loop
Append (Target => Target, Item => Bits.Instance (0));
end loop;
end;
end Message_Blocks;
-- Message lengths implementation
-- ========================================================================
package body Message_Lengths is
procedure Initialize (Target : out Instance)
is begin
Target.P := (others => 0);
Target.Overflowed := False;
end;
pragma Assert
(Element_Type'Pos (Element_Type'First) <=
Increment_Type'Pos (Increment_Type'First)); -- H1
pragma Assert
(Increment_Type'Pos (Increment_Type'Last) <=
Element_Type'Pos (Element_Type'Last)); -- H2
procedure Increment
(Target : in out Instance; Increase : Increment_Type := 1)
is
use type Element_Type;
C : Element_Type; -- Carry
Y : Element_Type := Element_Type (Increase); -- Valid by H1,H2
P : Polynomial_Type renames Target.P;
begin
for I in reverse P'Range loop
-- Reverse: remember last index is left-most, thus lower element.
C := (if (Y <= Element_Type'Last - P (I)) then 0 else 1);
P (I) := P (I) + Y;
exit when C = 0;
Y := C;
end loop;
if C /= 0 then
Target.Overflowed := True;
end if;
end;
procedure Append
(Target : in out Blocks.Instance;
This : in Instance)
is begin
for I in Index_Type loop
declare
use type Blocks.Element_Type;
Item : Blocks.Element_Type :=
Blocks.Elements.Rot_R
(N => Blocks.Elements.Width,
X => This.P (I));
begin
for J in 1 .. Blocks.Elements.Width loop
Item := Blocks.Elements.Rot_L (N => 1, X => Item);
Blocks.Append
(Target => Target,
Item => Bits.Instance (Item and 1));
end loop;
end;
end loop;
end;
end Message_Lengths;
-- Message hashes implementation
-- ========================================================================
package body Hashes is
procedure Initialize (Target : out Instance)
is begin
Target := Initial_Value;
end;
-- Algorithm implementation
-- ---------------------------------------------------------------------
package body Algorithm is
use type Blocks.Index_Type;
pragma Assert (Blocks.Index_Type'First <= 0); -- H1
pragma Assert (15 <= Blocks.Index_Type'Last); -- H2
procedure Hash (Target : in out Result_Type; Block : Block_Type)
is
use type Shedules.Index_Type;
function M (I : Blocks.Index_Type) return Blocks.Element_Type
is (Blocks.Item (This => Block, I => I));
W : Shedules.Instance; -- [6.1]
V : Hashes.Registers_Type; -- {1}
-- 1. I-th working variables [2.2.1], [6.1]
begin
-- The outermost for-loop is omitted, as this outer iteration is
-- handled by the parser feeding the current message block `M`,
-- and which invoks this method.
W := (others => 0); -- Not required, but avoid a warning.
Step_1: for T in W'Range loop
W (T) :=
(case T is
when 0 .. 15 =>
M (Blocks.Index_Type (T)), -- Valid by H1,H2
when 16 .. 79 =>
Hashes.Elements.Rot_L
(N => 1,
X =>
W (T - 3) xor
W (T - 8) xor
W (T - 14) xor
W (T - 16)));
end loop Step_1;
-- Assertions before iterations:
-- M(0..15) valid (was assigned a value) {1}.
--
-- During each iteration:
-- T in 16..79 => T - 16..3 valid indexes in W {2}.
--
-- At the end of each iteration:
-- T in 0..15 and M(T) is valid => W(0..T) valid {3}.
-- (15 <= T) => W(0..15) valid.
-- T = 16 and W(0..15) valid => W(0..15) and W(T) valid {4}.
-- T = 16 and W(0..15) valid => W(0..16) valid {5}.
-- T+0 = 16+0 and W(0..15+0) valid => W(0..15+0+1) valid {5}.
-- T+N = 16+N and W(0..15+N) valid => W(0..15+N+1) valid {6}.
-- … which allows to prove it for all T in 16 .. 78.
--
-- Conclusion:
-- No out of bounds index and all W items are assigned valid
-- values. For this reason, initialization of W prior to the loop
-- is not needed (but some compilers may not guess it).
--
-- 1. If the caller is not wrong, or else, there are garbages in M
-- and the hash is not meaningful. The precondition tries to
-- ensure Input (and thus M) was fully filled up.
-- 2. No index out of bounds during iterations.
-- 3. By copy from M(T) which is known (or supposed) to be valid.
-- 4. W(T) is computed from values which are known to be valid and
-- so is W(T).
-- 5. Rewording of the same.
-- 6. Inductive transition.
Step_2: begin
V := Target;
end Step_2;
Step_3: declare
Temp : Hashes.Element_Type; -- {1}
A : Hashes.Element_Type renames V (0);
B : Hashes.Element_Type renames V (1);
C : Hashes.Element_Type renames V (2);
D : Hashes.Element_Type renames V (3);
E : Hashes.Element_Type renames V (4);
-- 1. Temporary w-bit element [2.2.1], [6.1]
begin
for T in Message_Shedules.Index_Type loop
Temp :=
(Hashes.Elements.Rot_L (N => 5, X => A) +
F (T => T, X => B, Y => C, Z => D) +
E + Shedules.K (T) + W (T));
E := D;
D := C;
C := Hashes.Elements.Rot_L (N => 30, X => B);
B := A;
A := Temp;
end loop;
end Step_3;
Step_4: begin
-- New value is written in place of the old one, because the
-- old one is not referred to any more passed this point and
-- the new value is the future old value.
for I in Target'Range loop
Target (I) := Target (I) + V (I);
end loop;
end Step_4;
end Hash;
end Algorithm;
-- Texts implementation
-- ---------------------------------------------------------------------
package body Texts is
pragma Assert ((Elements.Width mod Base.Width) = 0); -- H1
pragma Assert
(((Text_Type'Last - Text_Type'First + 1) mod
(Elements.Width / Base.Width)) = 0); -- H2
pragma Assert
(((Index_Type'Pos (Instance'Last) -
Index_Type'Pos (Instance'First) + 1) *
(Elements.Width / Base.Width)) =
(Text_Type'Last - Text_Type'First + 1)); -- H3
procedure Write (Target : out Text_Type; Item : Instance)
is
subtype Base_Type is Base.Instance;
W : constant := Elements.Width / Base.Width; -- Valid by H1
M : constant := Base_Type'Modulus;
S : Text_Type renames Target;
P : Instance renames Item;
C : Element_Type;
K : Text_Index_Type := S'First;
begin
for I in P'Range loop -- Valid by H3
C := P (I);
declare
N : Base_Type;
begin
K := K + (W - 1); -- Valid by H2,H3
for J in 1 .. W loop -- Valid by H2
N := Base_Type (C mod M); -- Valid as M is type's modulus
C := C / M;
S (K) := Digit (N);
if not (J = W) then
K := K - 1;
end if;
end loop;
if not (I = P'Last) then
K := K + W; -- Valid by H2,H3
end if;
end;
end loop;
end Write;
end Texts;
end Hashes;
-- Message parsers implementation
-- ========================================================================
package body Parsers is
package Algorithm renames Hashes.Algorithm;
-- State and resources management
-- ---------------------------------------------------------------------
function Block_Length (This : Instance) return Blocks.Bit_Count_Type
is (Blocks.Length (This.Block));
procedure Next_Block (Target : in out Instance)
with Pre => Blocks.Is_Full (Target.Block);
procedure Last_Block (Target : in out Instance)
with Pre => Blocks.Is_Full (Target.Block);
procedure Release_Block (Target : in out Instance);
procedure Initialize (Target : out Instance)
is begin
Hashes.Initialize (Target.Hash);
Lengths.Initialize (Target.Length);
Blocks.Initialize (Target.Block);
Target.State := Initialized;
end;
procedure Next_Block (Target : in out Instance)
is begin
Algorithm.Hash (Target => Target.Hash, Block => Target.Block);
Blocks.Initialize (Target.Block);
end;
procedure Last_Block (Target : in out Instance)
is begin
Algorithm.Hash (Target => Target.Hash, Block => Target.Block);
Release_Block (Target);
end;
procedure Release_Block (Target : in out Instance)
is begin
-- Placeholder for potential future implementation variations.
null;
end;
-- Message parsing methods
-- ---------------------------------------------------------------------
use type Lengths.Instance;
use type Hashes.Instance;
use type Blocks.Bit_Count_Type;
procedure Append_Message_Bit
(Target : in out Instance;
Item : Bits.Instance)
with Post =>
(if Blocks.Is_Full (Target.Block'Old) and not Overflowed (Target)
then
Target.Hash /= Target.Hash'Old and -- {1}
Block_Length (Target) = 1 -- {2}
else Target.Hash = Target.Hash'Old);
-- 1. This means the block was hashed.
-- 2. This means a new block was started and the data appended to it.
procedure Append (Target : in out Instance; Item : Bits.Instance)
renames Append_Message_Bit;
use type Blocks.Bit_Count_Type;
use type Blocks.Index_Type;
procedure Append_Message_Bit
(Target : in out Instance;
Item : Bits.Instance)
is begin
-- When the current block appears to be full, we will hash this
-- current block and start a new one.
Target.State := Running;
if Lengths.Overflowed (Target.Length) then
return;
end if;
if Blocks.Is_Full (Target.Block) then
Next_Block (Target);
end if;
Blocks.Append (Target => Target.Block, Item => Item);
Lengths.Increment (Target => Target.Length, Increase => 1);
end;
-- Last block(s) finalization methods
-- ---------------------------------------------------------------------
procedure Pad_With_One (Target : in out Instance)
with
Pre => not Blocks.Is_Full (Target.Block),
Post => Block_Length (Target) = Block_Length (Target)'Old + 1;
procedure Pad_Width_Zeros
(Target : in out Instance;
Bound : Blocks.Bit_Count_Type)
with
Pre => Block_Length (Target) <= Bound,
Post => Block_Length (Target) = Bound;
procedure Pad_With_Length (Target : in out Instance)
with
Pre =>
Block_Length (Target) =
(Blocks.Bit_Count - Lengths.Bit_Count),
Post =>
Blocks.Is_Full (Target.Block);
procedure Pad_With_One (Target : in out Instance)
is begin
Blocks.Append (Target => Target.Block, Item => Bits.Instance (1));
end;
procedure Pad_Width_Zeros
(Target : in out Instance;
Bound : Blocks.Bit_Count_Type)
is begin
Blocks.Append_Zeros (Target => Target.Block, Bound => Bound);
end;
procedure Pad_With_Length (Target : in out Instance)
is begin
Lengths.Append (Target => Target.Block, This => Target.Length);
end;
pragma Assert (Lengths.Bit_Count < Blocks.Bit_Count); -- H1
procedure Finalize (Target : in out Instance) -- [5.1.1], [6.1.2]
is
Limit : constant := Blocks.Bit_Count - Lengths.Bit_Count;
-- Positive, by H1
begin
-- [5.1.1] says L + 1 + k ≡ 448 mod 512.
-- We won't even compute k, and instead add bits as necessary. This
-- will achieve the same: filling up to a length so that there
-- remains exactly the room to write the length, which will in turn
-- be the final padding to fill exactly up to the end of the block.
-- This is finally the purpose of the calculation of l, which needs
-- not be necessary calculated the way the specification suggest it.
if Lengths.Overflowed (Target.Length) then
Release_Block (Target);
Target.State := Invalid;
return;
end if;
if Blocks.Is_Full (Target.Block) then
Next_Block (Target);
end if;
Pad_With_One (Target => Target);
if Block_Length (Target) < Limit then
Pad_Width_Zeros (Target => Target, Bound => Limit);
elsif Block_Length (Target) = Limit then
null;
else -- if Target.B.L > Limit
Pad_Width_Zeros (Target => Target, Bound => Blocks.Bit_Count);
-- Block is full
Next_Block (Target);
Pad_Width_Zeros (Target => Target, Bound => Limit);
end if;
pragma Assert (Block_Length (Target) = Limit);
Pad_With_Length (Target);
pragma Assert (Blocks.Is_Full (Target.Block));
Last_Block (Target);
Target.State := Valid;
end;
end Parsers;
-- Items implementation
package body Items is
-- Single parser instance implementing the package's interface
-- ---------------------------------------------------------------------
Parser : Parsers.Instance;
function State return State_Type
is (Parsers.State (Parser));
procedure Initialize -- [5]
is begin
Parsers.Initialize (Parser);
end Initialize;
function Overflowed return Boolean
is (Parsers.Overflowed (Parser));
procedure Finalize
is begin
Parsers.Finalize (Parser);
end;
-- Static implementation for the generic Processors's `Append` methods
-- ---------------------------------------------------------------------
procedure Append
(Item : Widest_Binaries.Instance;
Length : Widest_Binaries.Bit_Count_Type)
is
package WB renames Widest_Binaries;
subtype Binary_Type is WB.Instance;
use type Binary_Type;
Binary : Binary_Type :=
(WB.Rot_R
(N => WB.Offset (Length),
X => Item));
begin
for I in 1 .. Length loop
Binary := WB.Rot_L (N => 1, X => Binary);
Parsers.Append
(Target => Parser,
Item => Bits.Instance (Binary and 1));
end loop;
end;
-- Processors implementation
-- ---------------------------------------------------------------------
package body Streamers is
package WB renames Widest_Binaries;
pragma Assert
(Bit_Count_Type'Pos (Bit_Count_Type'Last) <=
WB.Bit_Count_Type'Pos (WB.Bit_Count_Type'Last)); -- H1
pragma Assert
((Element_Type'Pos (Element_Type'Last) -
Element_Type'Pos (Element_Type'First)) <=
(WB.Instance'Pos (WB.Instance'Last))); -- H2
procedure Append
(Item : Element_Type;
Length : Bit_Count_Type := Bit_Count_Type'Last)
is
subtype Binary_Type is WB.Instance;
subtype Bit_Count_Type is WB.Bit_Count_Type;
Binary : constant Binary_Type :=
Binary_Type
(Element_Type'Pos (Item) -
Element_Type'Pos (Element_Type'First));
-- Valid by H2
begin
if 0 < Length then
Append
(Item => Binary,
Length => Bit_Count_Type (Length)); -- Valid by H1
end if;
end;
procedure Append
(Item : Array_Type;
First : Index_Type;
Last : Index_Type)
is begin
for I in First .. Last loop
Append (Item (I));
end loop;
end;
end Streamers;
-- Text methods implementation
-- ---------------------------------------------------------------------
procedure Write (Target : out Text_Type)
is begin
Hashes.Texts.Write
(Target => Target,
Item => Parsers.Result (Parser));
end;
function Text return Text_Type
is begin
return Result : Text_Type do
Write (Result);
end return;
end;
end Items;
end SHA1; Paquet offrant des instanciations typiques directement utilisablesSource Ada : -- Readily provided typical instantiations of `SHA1.Processors`.
with SHA1; -- For the generic package to be instantiated.
with Ada.Streams; -- For hashed items type
with System.Storage_Elements; -- For hashed items type
generic
-- Parameterless
package SHA1_Processors is
package Item is new SHA1.Items;
-- Incrementally hashing from stream elements
-- ========================================================================
type Stream_Element_Bit_Count_Type
is range 0 .. Ada.Streams.Stream_Element'Size;
package Stream_Streamer
is new Item.Streamers
(Bit_Count_Type => Stream_Element_Bit_Count_Type,
Element_Type => Ada.Streams.Stream_Element,
Index_Type => Ada.Streams.Stream_Element_Offset,
Array_Type => Ada.Streams.Stream_Element_Array);
-- Incrementally hashing from storage (memory) elements
-- ========================================================================
type Storage_Element_Bit_Count_Type
is range 0 .. System.Storage_Elements.Storage_Element'Size;
package Storage_Streamer
is new Item.Streamers
(Bit_Count_Type => Storage_Element_Bit_Count_Type,
Element_Type => System.Storage_Elements.Storage_Element,
Index_Type => System.Storage_Elements.Storage_Offset,
Array_Type => System.Storage_Elements.Storage_Array);
-- Incrementally hashing from characters (strings)
-- ========================================================================
type Character_Bit_Count_Type
is range 0 .. Character'Size;
package Character_Streamer
is new Item.Streamers
(Bit_Count_Type => Character_Bit_Count_Type,
Element_Type => Character,
Index_Type => Positive,
Array_Type => String);
end SHA1_Processors;
 Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon]
|
|
Administrateur
- Genre :
- Messages : 22324
|
Hibou a écrit : Dans le corps du paquet SHA1, des types ont été transformés en types opaques. Il en reste encore, mais ceux restant posent des problèmes d’organisation (des choses que je voudrais laisser dans leurs partis publiques, mais se retrouveraient dans leurs parties privés… des paradoxes ou des souhaits contradictoires à résoudre), alors ce n’est pas pour tout de suite. Je ne m’explique pas où je voyais un problème, et il me semble qu’il était évident que `SHA1.Parsers.Instance` devait être un type privé. Il est parfois bon de prendre de la distance et de revenir sur une chose après un certain temps, pour avoir une vue plus claire, sans avoir les pensées embrouillé par tout ce à quoi on peut penser quand on a la tête dans seau; c’est sûrement un n‑ième exemple de ce phénomène. J’ai un instant pensé à sortir `Hashes.Instance` de `SHA1.Parsers.Instance`, pensant qu’un `Parser` n’avait pas à posséder lui‑même une instance de `SHA1.Hashes.Instance`. Mais c’est finalement naturel qu’il le possède, pour deux raisons. La première, parce qu’il n’y a aucune raison de partager l’instance, et ça ne doit même surtout pas être possible; la seconde, parce qu’une vue fonctionnelle de ce qui est ici procédural, suggère bien que `SHA1.Hashes.Instance` est le résultat d’une fonction implicite `Parsed`, et que donc cette instance et entièrement crée à l’intérieur de cette fonction implicite `Parsed`. Le second message a été mise à jour en conséquence. En parlant de ce message, je crois que j’aurais dut faire trois messages séparée, un pour chacun des sources, mais c’est trop tard maintenant, car il n’est pas possible de re‑insérer un message avant un autre, et faudrait les anti‑dater, et ça n’est pas possible. Je ne suis pas encore satisfait de la forme actuelle, à cause des paramètres nommés `Target`, pour désigner les paramètres `in out`. Autant le `This` pour les paramètres `in` semble couler de source, autant `Target` fait référence à tout autre chose, et ne convient finalement pas. Je n’ai pas d’idée d’un autre nom pour l’instant (je sais seulement que le nom actuel ne convient pas et désigne mal la chose), alors je ne peux pas encore corriger ce défaut. Je reste également encore dans le doute sur le choix de `Instance` ou `Instance_Type` pour désigner le type défini par les paquets dont le sujet central est un type. `Instance_Type` a l’avantage de suivre la convention de nommage de tous les autres types, qui est de leur donner le suffixe `_Type` , mais remplacer tous les `Instance` par `Instance_Type` ajoute beaucoup du bruit aux sources, j’en ai l’impression. Je suis en même temps conscient que le premier point pèse plus que le second qui est moins un problème, et alors il y a de bonnes chances pour que les `Instance` soient tous renommés en `Instance_Type` dans une prochaine révision.
Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon]
|
Hachage SHA‑1 en Ada
, parce qu’elle est difficilement compatible avec l’idée d’une implémentation de référence… Je vais y réfléchir 
.
