updated eel and eapml from more recent versions.

This commit is contained in:
Jocelyn Fiat
2012-06-15 14:57:12 +02:00
parent 0203e0fdc7
commit 5f3749e463
166 changed files with 396 additions and 578 deletions

View File

@@ -0,0 +1,283 @@
note
description: "Objects that ..."
author: "Colin LeMahieu"
date: "$Date: 2011-11-11 18:13:16 +0100 (ven., 11 nov. 2011) $"
revision: "$Revision: 87787 $"
quote: "Blessed are the young, for they shall inherit the national debt. - Herbert Hoover"
class
MD5
inherit
ANY
redefine
is_equal
end
SHA_FUNCTIONS
rename
ch as f,
parity as h,
byte_sink as update
export
{MD5}
schedule,
buffer,
byte_count,
schedule_offset,
buffer_offset
undefine
is_equal
redefine
process_length,
process_word,
update_word
end
ROTATE_FACILITIES
undefine
is_equal
end
DEBUG_OUTPUT
undefine
is_equal
end
create
make,
make_copy
feature
make
do
create schedule.make_filled (0, 16)
create buffer.make_filled (0, 4)
reset
end
make_copy (other: like Current)
do
make
schedule.copy_data (other.schedule, other.schedule.lower, schedule.lower, schedule.count)
buffer.copy_data (other.buffer, other.buffer.lower, buffer.lower, buffer.count)
h1 := other.h1
h2 := other.h2
h3 := other.h3
h4 := other.h4
schedule_offset := other.schedule_offset
byte_count := other.byte_count
buffer_offset := other.buffer_offset
ensure
Current ~ other
end
feature
reset
do
byte_count := 0
schedule_offset := 0
buffer_offset := 0
h1 := 0x67452301
h2 := 0xefcdab89
h3 := 0x98badcfe
h4 := 0x10325476
ensure
byte_count = 0
schedule_offset = 0
buffer_offset = 0
h1 = 0x67452301
h2 = 0xefcdab89
h3 = 0x98badcfe
h4 = 0x10325476
end
do_final (output: SPECIAL [NATURAL_8] offset: INTEGER_32)
require
valid_start: output.valid_index (offset)
valid_end: output.valid_index (offset + 15)
do
finish
from_natural_32_le (h1, output, offset)
from_natural_32_le (h2, output, offset + 4)
from_natural_32_le (h3, output, offset + 8)
from_natural_32_le (h4, output, offset + 12)
reset
end
current_final (output: SPECIAL [NATURAL_8] offset: INTEGER_32)
require
valid_start: output.valid_index (offset)
valid_end: output.valid_index (offset + 15)
local
current_copy: like Current
do
create current_copy.make_copy (Current)
current_copy.do_final (output, offset)
end
current_out: STRING
local
output: SPECIAL [NATURAL_8]
index: INTEGER_32
do
Result := "0x"
create output.make_filled (0, 16)
current_final (output, 0)
from
index := 0
until
index = 16
loop
Result.append (output [index].to_hex_string)
index := index + 1
end
end
is_equal (other: like Current): BOOLEAN
do
Result :=
schedule.same_items (other.schedule, other.schedule.lower, schedule.lower, schedule.count) and
buffer.same_items (other.buffer, other.buffer.lower, buffer.lower, buffer.count) and
h1 = other.h1 and
h2 = other.h2 and
h3 = other.h3 and
h4 = other.h4 and
schedule_offset = other.schedule_offset and
byte_count = other.byte_count and
buffer_offset = other.buffer_offset
end
feature {NONE}
g (u: NATURAL_32 v: NATURAL_32 w: NATURAL_32): NATURAL_32
do
result := (u & w) | (v & w.bit_not)
end
k (u: NATURAL_32 v: NATURAL_32 w: NATURAL_32): NATURAL_32
do
result := v.bit_xor (u | w.bit_not)
end
process_length (length: NATURAL_64)
do
update_word (length.to_natural_32)
update_word ((length |>> 32).to_natural_32)
end
feature {NONE}
process_word (in: SPECIAL [NATURAL_8] offset: INTEGER_32)
do
schedule [schedule_offset] := as_natural_32_le (in, offset)
schedule_offset := schedule_offset + 1
if
schedule_offset = 16
then
schedule_offset := 0
process_block
end
end
update_word (in: NATURAL_32)
do
update (in.to_natural_8)
update ((in |>> 8).to_natural_8)
update ((in |>> 16).to_natural_8)
update ((in |>> 24).to_natural_8)
end
process_block
do
a := h1
b := h2
c := h3
d := h4
a := rotate_left_32 (a + f (b, c, d) + schedule [0] + 0xd76aa478, 7) + b
d := rotate_left_32 (d + f (a, b, c) + schedule [1] + 0xe8c7b756, 12) + a
c := rotate_left_32 (c + f (d, a, b) + schedule [2] + 0x242070db, 17) + d
b := rotate_left_32 (b + f (c, d, a) + schedule [3] + 0xc1bdceee, 22) + c
a := rotate_left_32 (a + f (b, c, d) + schedule [4] + 0xf57c0faf, 7) + b
d := rotate_left_32 (d + f (a, b, c) + schedule [5] + 0x4787c62a, 12) + a
c := rotate_left_32 (c + f (d, a, b) + schedule [6] + 0xa8304613, 17) + d
b := rotate_left_32 (b + f (c, d, a) + schedule [7] + 0xfd469501, 22) + c
a := rotate_left_32 (a + f (b, c, d) + schedule [8] + 0x698098d8, 7) + b
d := rotate_left_32 (d + f (a, b, c) + schedule [9] + 0x8b44f7af, 12) + a
c := rotate_left_32 (c + f (d, a, b) + schedule [10] + 0xffff5bb1, 17) + d
b := rotate_left_32 (b + f (c, d, a) + schedule [11] + 0x895cd7be, 22) + c
a := rotate_left_32 (a + f (b, c, d) + schedule [12] + 0x6b901122, 7) + b
d := rotate_left_32 (d + f (a, b, c) + schedule [13] + 0xfd987193, 12) + a
c := rotate_left_32 (c + f (d, a, b) + schedule [14] + 0xa679438e, 17) + d
b := rotate_left_32 (b + f (c, d, a) + schedule [15] + 0x49b40821, 22) + c
a := rotate_left_32 (a + g (b, c, d) + schedule [1] + 0xf61e2562, 5) + b
d := rotate_left_32 (d + g (a, b, c) + schedule [6] + 0xc040b340, 9) + a
c := rotate_left_32 (c + g (d, a, b) + schedule [11] + 0x265e5a51, 14) + d
b := rotate_left_32 (b + g (c, d, a) + schedule [0] + 0xe9b6c7aa, 20) + c
a := rotate_left_32 (a + g (b, c, d) + schedule [5] + 0xd62f105d, 5) + b
d := rotate_left_32 (d + g (a, b, c) + schedule [10] + 0x02441453, 9) + a
c := rotate_left_32 (c + g (d, a, b) + schedule [15] + 0xd8a1e681, 14) + d
b := rotate_left_32 (b + g (c, d, a) + schedule [4] + 0xe7d3fbc8, 20) + c
a := rotate_left_32 (a + g (b, c, d) + schedule [9] + 0x21e1cde6, 5) + b
d := rotate_left_32 (d + g (a, b, c) + schedule [14] + 0xc33707d6, 9) + a
c := rotate_left_32 (c + g (d, a, b) + schedule [3] + 0xf4d50d87, 14) + d
b := rotate_left_32 (b + g (c, d, a) + schedule [8] + 0x455a14ed, 20) + c
a := rotate_left_32 (a + g (b, c, d) + schedule [13] + 0xa9e3e905, 5) + b
d := rotate_left_32 (d + g (a, b, c) + schedule [2] + 0xfcefa3f8, 9) + a
c := rotate_left_32 (c + g (d, a, b) + schedule [7] + 0x676f02d9, 14) + d
b := rotate_left_32 (b + g (c, d, a) + schedule [12] + 0x8d2a4c8a, 20) + c
a := rotate_left_32 (a + h (b, c, d) + schedule [5] + 0xfffa3942, 4) + b
d := rotate_left_32 (d + h (a, b, c) + schedule [8] + 0x8771f681, 11) + a
c := rotate_left_32 (c + h (d, a, b) + schedule [11] + 0x6d9d6122, 16) + d
b := rotate_left_32 (b + h (c, d, a) + schedule [14] + 0xfde5380c, 23) + c
a := rotate_left_32 (a + h (b, c, d) + schedule [1] + 0xa4beea44, 4) + b
d := rotate_left_32 (d + h (a, b, c) + schedule [4] + 0x4bdecfa9, 11) + a
c := rotate_left_32 (c + h (d, a, b) + schedule [7] + 0xf6bb4b60, 16) + d
b := rotate_left_32 (b + h (c, d, a) + schedule [10] + 0xbebfbc70, 23) + c
a := rotate_left_32 (a + h (b, c, d) + schedule [13] + 0x289b7ec6, 4) + b
d := rotate_left_32 (d + h (a, b, c) + schedule [0] + 0xeaa127fa, 11) + a
c := rotate_left_32 (c + h (d, a, b) + schedule [3] + 0xd4ef3085, 16) + d
b := rotate_left_32 (b + h (c, d, a) + schedule [6] + 0x04881d05, 23) + c
a := rotate_left_32 (a + h (b, c, d) + schedule [9] + 0xd9d4d039, 4) + b
d := rotate_left_32 (d + h (a, b, c) + schedule [12] + 0xe6db99e5, 11) + a
c := rotate_left_32 (c + h (d, a, b) + schedule [15] + 0x1fa27cf8, 16) + d
b := rotate_left_32 (b + h (c, d, a) + schedule [2] + 0xc4ac5665, 23) + c
a := rotate_left_32 (a + k (b, c, d) + schedule [0] + 0xf4292244, 6) + b
d := rotate_left_32 (d + k (a, b, c) + schedule [7] + 0x432aff97, 10) + a
c := rotate_left_32 (c + k (d, a, b) + schedule [14] + 0xab9423a7, 15) + d
b := rotate_left_32 (b + k (c, d, a) + schedule [5] + 0xfc93a039, 21) + c
a := rotate_left_32 (a + k (b, c, d) + schedule [12] + 0x655b59c3, 6) + b
d := rotate_left_32 (d + k (a, b, c) + schedule [3] + 0x8f0ccc92, 10) + a
c := rotate_left_32 (c + k (d, a, b) + schedule [10] + 0xffeff47d, 15) + d
b := rotate_left_32 (b + k (c, d, a) + schedule [1] + 0x85845dd1, 21) + c
a := rotate_left_32 (a + k (b, c, d) + schedule [8] + 0x6fa87e4f, 6) + b
d := rotate_left_32 (d + k (a, b, c) + schedule [15] + 0xfe2ce6e0, 10) + a
c := rotate_left_32 (c + k (d, a, b) + schedule [6] + 0xa3014314, 15) + d
b := rotate_left_32 (b + k (c, d, a) + schedule [13] + 0x4e0811a1, 21) + c
a := rotate_left_32 (a + k (b, c, d) + schedule [4] + 0xf7537e82, 6) + b
d := rotate_left_32 (d + k (a, b, c) + schedule [11] + 0xbd3af235, 10) + a
c := rotate_left_32 (c + k (d, a, b) + schedule [2] + 0x2ad7d2bb, 15) + d
b := rotate_left_32 (b + k (c, d, a) + schedule [9] + 0xeb86d391, 21) + c
h1 := h1 + a
h2 := h2 + b
h3 := h3 + c
h4 := h4 + d
end
a: NATURAL_32
b: NATURAL_32
c: NATURAL_32
d: NATURAL_32
feature -- {DEBUG_OUTPUT}
debug_output: STRING
do
Result := current_out
end
feature {MD5}
h1: NATURAL_32
h2: NATURAL_32
h3: NATURAL_32
h4: NATURAL_32
end

View File

@@ -0,0 +1,346 @@
note
description: "Objects that ..."
author: "Colin LeMahieu"
date: "$Date: 2011-11-11 18:13:16 +0100 (ven., 11 nov. 2011) $"
revision: "$Revision: 87787 $"
quote: "There's never been a good government. - Emma Goldman"
class
SHA1
inherit
ANY
redefine
is_equal
end
DEBUG_OUTPUT
undefine
is_equal
end
SHA_FUNCTIONS
rename
byte_sink as update
export
{SHA1}
schedule,
buffer,
byte_count,
schedule_offset,
buffer_offset
undefine
is_equal
end
ROTATE_FACILITIES
undefine
is_equal
end
create
make,
make_copy
feature -- Creation
make
do
create schedule.make_filled (0, 80)
create buffer.make_filled (0, 4)
buffer_offset := 0
reset
end
make_copy (other: like Current)
do
make
schedule.copy_data (other.schedule, other.schedule.lower, schedule.lower, schedule.count)
buffer.copy_data (other.buffer, other.buffer.lower, buffer.lower, buffer.count)
byte_count := other.byte_count
buffer_offset := other.buffer_offset
h1 := other.h1
h2 := other.h2
h3 := other.h3
h4 := other.h4
h5 := other.h5
schedule_offset := other.schedule_offset
ensure
Current ~ other
end
feature -- Implementing DIGEST
reset
do
byte_count := 0
buffer_offset := 0
h1 := 0x67452301
h2 := 0xefcdab89
h3 := 0x98badcfe
h4 := 0x10325476
h5 := 0xc3d2e1f0
schedule_offset := 0
ensure
byte_count = 0
buffer_offset = 0
schedule_offset = 0
h1 = 0x67452301
h2 = 0xefcdab89
h3 = 0x98badcfe
h4 = 0x10325476
h5 = 0xc3d2e1f0
end
do_final (output: SPECIAL [NATURAL_8] offset: INTEGER)
require
valid_start: output.valid_index (offset)
valid_end: output.valid_index (offset + 19)
do
finish
unpack_word (h1, output, offset)
unpack_word (h2, output, offset + 4)
unpack_word (h3, output, offset + 8)
unpack_word (h4, output, offset + 12)
unpack_word (h5, output, offset + 16)
reset
end
current_final (output: SPECIAL [NATURAL_8] offset: INTEGER_32)
require
valid_start: output.valid_index (offset)
valid_end: output.valid_index (offset + 19)
local
current_copy: like Current
do
current_copy := Current.deep_twin
current_copy.do_final (output, offset)
end
current_out: STRING
local
output: SPECIAL [NATURAL_8]
index: INTEGER_32
do
Result := "0x"
create output.make_filled (0, 20)
current_final (output, 0)
from
index := 0
until
index = 20
loop
Result.append (output [index].to_hex_string)
index := index + 1
end
end
is_equal (other: like Current): BOOLEAN
do
Result :=
schedule.same_items (other.schedule, other.schedule.lower, schedule.lower, schedule.count) and
buffer.same_items (other.buffer, other.buffer.lower, buffer.lower, buffer.count) and
h1 = other.h1 and
h2 = other.h2 and
h3 = other.h3 and
h4 = other.h4 and
h5 = other.h5 and
schedule_offset = other.schedule_offset and
byte_count = other.byte_count and
buffer_offset = other.buffer_offset
end
feature {NONE}
unpack_word (word: NATURAL_32 output: SPECIAL [NATURAL_8] offset: INTEGER)
require
valid_start: output.valid_index (offset)
valid_end: output.valid_index (offset + 3)
do
output [offset] := (word |>> 24).to_natural_8
output [offset + 1] := (word |>> 16).to_natural_8
output [offset + 2] := (word |>> 8).to_natural_8
output [offset + 3] := word.to_natural_8
end
A: NATURAL_32
B: NATURAL_32
C: NATURAL_32
D: NATURAL_32
E: NATURAL_32
process_block
do
expand_word_block
A := H1
B := H2
C := H3
D := H4
E := H5
do_round_1
do_round_2
do_round_3
do_round_4
h1 := h1 + a
h2 := h2 + b
h3 := h3 + c
h4 := h4 + d
h5 := h5 + e
end
do_round_4
local
j: INTEGER
idx: INTEGER
do
idx := 60
from
j := 0
until
j = 4
loop
e := e + rotate_left_32 (a, 5) + parity (b, c, d) + schedule [idx] + k4
idx := idx + 1
b := rotate_left_32 (b, 30)
d := d + rotate_left_32 (e, 5) + parity (a, b, c) + schedule [idx] + k4
idx := idx + 1
a := rotate_left_32 (a, 30)
c := c + rotate_left_32 (d, 5) + parity (e, a, b) + schedule [idx] + k4
idx := idx + 1
e := rotate_left_32 (e, 30)
b := b + rotate_left_32 (c, 5) + parity (d, e, a) + schedule [idx] + k4
idx := idx + 1
d := rotate_left_32 (d, 30)
a := a + rotate_left_32 (b, 5) + parity (c, d, e) + schedule [idx] + k4
idx := idx + 1
c := rotate_left_32 (c, 30)
j := j + 1
end
end
do_round_3
local
j: INTEGER
idx: INTEGER
do
idx := 40
from
j := 0
until
j = 4
loop
E := E + rotate_left_32 (a, 5) + maj (B, C, D) + schedule [idx] + k3
idx := idx + 1
B := rotate_left_32 (b, 30)
D := d + rotate_left_32 (e, 5) + maj (a, b, c) + schedule [idx] + k3
idx := idx + 1
A := rotate_left_32 (a, 30)
C := C + rotate_left_32 (d, 5) + maj (e, a, b) + schedule [idx] + k3
idx := idx + 1
e := rotate_left_32 (e, 30)
b := b + rotate_left_32 (c, 5) + maj (d, e, a) + schedule [idx] + k3
idx := idx + 1
d := rotate_left_32 (d, 30)
a := a + rotate_left_32 (b, 5) + maj (c, d, e) + schedule [idx] + k3
idx := idx + 1
c := rotate_left_32 (c, 30)
j := j + 1
end
end
do_round_2
local
j: INTEGER
idx: INTEGER
do
idx := 20
from
j := 0
until
j = 4
loop
E := E + rotate_left_32 (a, 5) + parity(B, C, D) + schedule [idx] + k2
idx := idx + 1
B := rotate_left_32 (b, 30)
D := d + rotate_left_32 (e, 5) + parity(a, b, c) + schedule [idx] + k2
idx := idx + 1
A := rotate_left_32 (a, 30)
C := C + rotate_left_32 (d, 5) + parity(e, a, b) + schedule [idx] + k2
idx := idx + 1
e := rotate_left_32 (e, 30)
b := b + rotate_left_32 (c, 5) + parity(d, e, a) + schedule [idx] + k2
idx := idx + 1
d := rotate_left_32 (d, 30)
a := a + rotate_left_32 (b, 5) + parity(c, d, e) + schedule [idx] + k2
idx := idx + 1
c := rotate_left_32 (c, 30)
j := j + 1
end
end
do_round_1
local
j: INTEGER
idx: INTEGER
do
idx := 0
from
j := 0
until
j = 4
loop
E := E + rotate_left_32 (a, 5) + ch (B, C, D) + schedule [idx] + k1
idx := idx + 1
B := rotate_left_32 (b, 30)
D := d + rotate_left_32 (e, 5) + ch (a, b, c) + schedule [idx] + k1
idx := idx + 1
A := rotate_left_32 (a, 30)
C := C + rotate_left_32 (d, 5) + ch (e, a, b) + schedule [idx] + k1
idx := idx + 1
e := rotate_left_32 (e, 30)
b := b + rotate_left_32 (c, 5) + ch (d, e, a) + schedule [idx] + k1
idx := idx + 1
d := rotate_left_32 (d, 30)
a := a + rotate_left_32 (b, 5) + ch (c, d, e) + schedule [idx] + k1
idx := idx + 1
c := rotate_left_32 (c, 30)
j := j + 1
end
end
expand_word_block
-- Expand 16 word block in to 80 word block
local
i: INTEGER
temp: NATURAL_32
do
from
i := 16
until
i = 80
loop
temp := schedule [i - 3].bit_xor (schedule [i - 8]).bit_xor (schedule [i - 14]).bit_xor (schedule [i - 16])
schedule [i] := rotate_left_32 (temp, 1)
i := i + 1
end
end
feature {SHA1}
H1: NATURAL_32
H2: NATURAL_32
H3: NATURAL_32
H4: NATURAL_32
H5: NATURAL_32
feature {NONE}
k1: NATURAL_32 = 0x5a827999
k2: NATURAL_32 = 0x6ed9eba1
k3: NATURAL_32 = 0x8f1bbcdc
k4: NATURAL_32 = 0xca62c1d6
feature {DEBUG_OUTPUT} -- {DEBUG_OUTPUT}
debug_output: STRING
do
result := current_out
end
invariant
schedule_lower:schedule.lower = 0
schedule_upper:schedule.upper = 79
end

View File

@@ -0,0 +1,363 @@
note
description: "Objects that ..."
author: "Colin LeMahieu"
date: "$Date: 2011-11-11 18:13:16 +0100 (ven., 11 nov. 2011) $"
revision: "$Revision: 87787 $"
quote: "Useless laws weaken the necessary laws. - Montesquieu"
class
SHA256
inherit
ANY
redefine
is_equal
end
DEBUG_OUTPUT
undefine
is_equal
end
SHA_FUNCTIONS
rename
byte_sink as update
export
{SHA256}
schedule,
buffer,
schedule_offset,
byte_count,
buffer_offset
undefine
is_equal
end
ROTATE_FACILITIES
undefine
is_equal
end
create
make,
make_copy
feature
make
do
create schedule.make_filled (0, 64)
create buffer.make_filled (0, 4)
reset
end
make_copy (other: like Current)
do
make
schedule.copy_data (other.schedule, other.schedule.lower, schedule.lower, schedule.count)
buffer.copy_data (other.buffer, other.buffer.lower, buffer.lower, buffer.count)
byte_count := other.byte_count
buffer_offset := other.buffer_offset
h1 := other.h1
h2 := other.h2
h3 := other.h3
h4 := other.h4
h5 := other.h5
h6 := other.h6
h7 := other.h7
h8 := other.h8
schedule_offset := other.schedule_offset
ensure
Current ~ other
end
feature
do_final (output: SPECIAL[NATURAL_8] out_off: INTEGER)
require
valid_offset: out_off >= 0
out_big_enough: out.count - out_off >= 32
do
finish
from_natural_32_be (h1, output, out_off)
from_natural_32_be (h2, output, out_off + 4)
from_natural_32_be (h3, output, out_off + 8)
from_natural_32_be (h4, output, out_off + 12)
from_natural_32_be (h5, output, out_off + 16)
from_natural_32_be (h6, output, out_off + 20)
from_natural_32_be (h7, output, out_off + 24)
from_natural_32_be (h8, output, out_off + 28)
reset
end
reset
do
buffer_offset := 0
h1 := 0x6a09e667
h2 := 0xbb67ae85
h3 := 0x3c6ef372
h4 := 0xa54ff53a
h5 := 0x510e527f
h6 := 0x9b05688c
h7 := 0x1f83d9ab
h8 := 0x5be0cd19
schedule_offset := 0
schedule.fill_with ({NATURAL_32} 0, 0, schedule.upper)
ensure
buffer_reset: buffer_offset = 0
schedule_reset: schedule_offset = 0
end
current_final (output: SPECIAL [NATURAL_8] offset: INTEGER_32)
require
valid_start: output.valid_index (offset)
valid_end: output.valid_index (offset + 31)
local
current_copy: like Current
do
current_copy := Current.deep_twin
current_copy.do_final (output, offset)
end
current_out: STRING
local
output: SPECIAL [NATURAL_8]
index: INTEGER_32
do
Result := "0x"
create output.make_filled (0, 32)
current_final (output, 0)
from
index := 0
until
index = 32
loop
Result.append (output [index].to_hex_string)
index := index + 1
end
end
is_equal (other: like Current): BOOLEAN
do
Result :=
schedule.same_items (other.schedule, other.schedule.lower, schedule.lower, schedule.count) and
buffer.same_items (other.buffer, other.buffer.lower, buffer.lower, buffer.count) and
h1 = other.h1 and
h2 = other.h2 and
h3 = other.h3 and
h4 = other.h4 and
h5 = other.h5 and
h6 = other.h6 and
h7 = other.h7 and
h8 = other.h8 and
schedule_offset = other.schedule_offset and
byte_count = other.byte_count and
buffer_offset = other.buffer_offset
end
feature{NONE}
process_block
local
a: NATURAL_32
b: NATURAL_32
c: NATURAL_32
d: NATURAL_32
e: NATURAL_32
f: NATURAL_32
g: NATURAL_32
h: NATURAL_32
t: INTEGER
i: INTEGER
do
expand_blocks
a := h1
b := h2
c := h3
d := h4
e := h5
f := h6
g := h7
h := h8
t := 0
from
i := 0
until
i = 8
loop
h := h + sigma1 (e) + ch (e, f, g) + k [t] + schedule [t]
t := t + 1
d := d + h
h := h + sigma0 (a) + maj (a, b, c)
g := g + sigma1 (d) + ch (d, e, f) + k [t] + schedule [t]
t := t + 1
c := c + g
g := g + sigma0 (h) + maj (h, a, b)
f := f + sigma1 (c) + ch (c, d, e) + k [t] + schedule [t]
t := t + 1
b := b + f
f := f + sigma0 (g) + maj (g, h, a)
e := e + sigma1 (b) + ch (b, c, d) + k [t] + schedule [t]
t := t + 1
a := a + e
e := e + sigma0 (f) + maj (f, g, h)
d := d + sigma1 (a) + ch (a, b, c) + k [t] + schedule [t]
t := t + 1
h := h + d
d := d + sigma0 (e) + maj (e, f, g)
c := c + sigma1 (h) + ch (h, a, b) + k [t] + schedule [t]
t := t + 1
g := g + c
c := c + sigma0 (d) + maj (d, e, f)
b := b + sigma1 (g) + ch (g, h, a) + k [t] + schedule [t]
t := t + 1
f := f + b
b := b + sigma0 (c) + maj (c, d, e)
a := a + sigma1 (f) + ch (f, g, h) + k [t] + schedule [t]
t := t + 1
e := e + a
a := a + sigma0 (b) + maj (b, c, d)
i := i + 1
end
h1 := h1 + a
h2 := h2 + b
h3 := h3 + c
h4 := h4 + d
h5 := h5 + e
h6 := h6 + f
h7 := h7 + g
h8 := h8 + h
end
sigma0 (x1: NATURAL_32): NATURAL_32
do
result := rotate_right_32 (x1, 2)
result := result.bit_xor (rotate_right_32 (x1, 13))
result := result.bit_xor (rotate_right_32 (x1, 22))
end
sigma1 (x1: NATURAL_32): NATURAL_32
do
result := rotate_right_32 (x1, 6)
result := result.bit_xor (rotate_right_32 (x1, 11))
result := result.bit_xor (rotate_right_32 (x1, 25))
end
lsigma0(x1: NATURAL_32): NATURAL_32
do
result := (rotate_right_32 (x1, 7)).bit_xor (rotate_right_32 (x1, 18)).bit_xor (x1 |>> 3)
end
lsigma1(x1: NATURAL_32): NATURAL_32
do
result := (rotate_right_32 (x1, 17)).bit_xor (rotate_right_32 (x1, 19)).bit_xor (x1 |>> 10)
end
expand_blocks
local
t: INTEGER
do
from
t := 16
until
t = 64
loop
schedule[t] := lsigma1 (schedule [t - 2]) + schedule [t - 7] + lsigma0 (schedule [t - 15]) + schedule [t - 16]
t := t + 1
end
end
k: SPECIAL[NATURAL_32]
once
create result.make_filled (0, 64)
result[0] := 0x428a2f98
result[1] := 0x71374491
result[2] := 0xb5c0fbcf
result[3] := 0xe9b5dba5
result[4] := 0x3956c25b
result[5] := 0x59f111f1
result[6] := 0x923f82a4
result[7] := 0xab1c5ed5
result[8] := 0xd807aa98
result[9] := 0x12835b01
result[10] := 0x243185be
result[11] := 0x550c7dc3
result[12] := 0x72be5d74
result[13] := 0x80deb1fe
result[14] := 0x9bdc06a7
result[15] := 0xc19bf174
result[16] := 0xe49b69c1
result[17] := 0xefbe4786
result[18] := 0x0fc19dc6
result[19] := 0x240ca1cc
result[20] := 0x2de92c6f
result[21] := 0x4a7484aa
result[22] := 0x5cb0a9dc
result[23] := 0x76f988da
result[24] := 0x983e5152
result[25] := 0xa831c66d
result[26] := 0xb00327c8
result[27] := 0xbf597fc7
result[28] := 0xc6e00bf3
result[29] := 0xd5a79147
result[30] := 0x06ca6351
result[31] := 0x14292967
result[32] := 0x27b70a85
result[33] := 0x2e1b2138
result[34] := 0x4d2c6dfc
result[35] := 0x53380d13
result[36] := 0x650a7354
result[37] := 0x766a0abb
result[38] := 0x81c2c92e
result[39] := 0x92722c85
result[40] := 0xa2bfe8a1
result[41] := 0xa81a664b
result[42] := 0xc24b8b70
result[43] := 0xc76c51a3
result[44] := 0xd192e819
result[45] := 0xd6990624
result[46] := 0xf40e3585
result[47] := 0x106aa070
result[48] := 0x19a4c116
result[49] := 0x1e376c08
result[50] := 0x2748774c
result[51] := 0x34b0bcb5
result[52] := 0x391c0cb3
result[53] := 0x4ed8aa4a
result[54] := 0x5b9cca4f
result[55] := 0x682e6ff3
result[56] := 0x748f82ee
result[57] := 0x78a5636f
result[58] := 0x84c87814
result[59] := 0x8cc70208
result[60] := 0x90befffa
result[61] := 0xa4506ceb
result[62] := 0xbef9a3f7
result[63] := 0xc67178f2
end
feature {SHA256}
h1: NATURAL_32
h2: NATURAL_32
h3: NATURAL_32
h4: NATURAL_32
h5: NATURAL_32
h6: NATURAL_32
h7: NATURAL_32
h8: NATURAL_32
feature {NONE} -- {DEBUG_OUTPUT}
debug_output: STRING
do
result := current_out
end
invariant
buffer_size: buffer.count = 4
valid_buffer_offset: buffer.valid_index (buffer_offset)
schedule_size: schedule.count = 64
valid_schedule_offset: schedule.valid_index (schedule_offset)
end

View File

@@ -0,0 +1,118 @@
note
description: "Summary description for {SHA_FUNCTIONS}."
author: "Colin LeMahieu"
date: "$Date: 2011-11-11 18:13:16 +0100 (ven., 11 nov. 2011) $"
revision: "$Revision: 87787 $"
quote: "The war for freedom will never really be won because the price of our freedom is constant vigilance over ourselves and over our Government. - Eleanor Roosevelt"
deferred class
SHA_FUNCTIONS
inherit
BYTE_FACILITIES
BYTE_32_BIT_BLOCK_FACILITIES
redefine
update
end
feature {NONE}
ch (u: NATURAL_32 v: NATURAL_32 w: NATURAL_32): NATURAL_32
do
result := (u & v) | (u.bit_not & w)
end
maj (u: NATURAL_32 v: NATURAL_32 w: NATURAL_32): NATURAL_32
do
result := (u & v) | (u & w) | (v & w)
end
parity (u: NATURAL_32 v: NATURAL_32 w: NATURAL_32): NATURAL_32
do
result := u.bit_xor (v).bit_xor (w)
end
feature {NONE} -- Padding facilities
pad
local
pad_bytes: INTEGER_32
do
update (0b1000_0000)
from
pad_bytes := (56 - (byte_count \\ 64)).to_integer_32
if
pad_bytes < 0
then
pad_bytes := pad_bytes + 64
end
until
pad_bytes = 0
loop
update (0)
pad_bytes := pad_bytes - 1
end
end
byte_count: NATURAL_64
bit_count: NATURAL_64
do
result := byte_count |<< 3
end
update (in: NATURAL_8)
do
precursor (in)
byte_count := byte_count + 1
ensure then
byte_count = old byte_count + 1
end
feature {NONE} -- Length processing facilities
process_length (length: NATURAL_64)
require
schedule_start: schedule_offset = 14
empty_buffer: buffer_offset = 0
do
update_word ((length |>> 32).to_natural_32)
update_word (length.to_natural_32)
ensure
empty_buffer: buffer_offset = 0
schedule_end: schedule_offset = 0
end
process_word (in: SPECIAL [NATURAL_8] offset: INTEGER_32)
do
schedule [schedule_offset] := as_natural_32_be (in, offset)
schedule_offset := schedule_offset + 1
if
schedule_offset = 16
then
schedule_offset := 0
process_block
end
end
process_block
deferred
end
finish
local
length: NATURAL_64
do
length := bit_count
pad
process_length (length)
end
feature {NONE}
schedule: SPECIAL [NATURAL_32]
schedule_offset: INTEGER_32
invariant
valid_schedule_offset: schedule.valid_index (schedule_offset)
valid_schedule_offset_lower: schedule_offset >= 0
valid_schedule_offset_upper: schedule_offset <= 15
valid_schedule_lower: schedule.valid_index (0)
valid_schedule_upper: schedule.valid_index (15)
end

View File

@@ -0,0 +1,118 @@
note
description: "Summary description for {SHA_FUNCTIONS}."
author: "Colin LeMahieu"
date: "$Date$"
revision: "$Revision$"
quote: "The war for freedom will never really be won because the price of our freedom is constant vigilance over ourselves and over our Government. - Eleanor Roosevelt"
deferred class
SHA_FUNCTIONS
inherit
BYTE_FACILITIES
BYTE_32_BIT_BLOCK_FACILITIES
redefine
update
end
feature {NONE}
ch (u: NATURAL_32; v: NATURAL_32; w: NATURAL_32): NATURAL_32 is
do
result := (u & v) | (u.bit_not & w)
end
maj (u: NATURAL_32; v: NATURAL_32; w: NATURAL_32): NATURAL_32 is
do
result := (u & v) | (u & w) | (v & w)
end
parity (u: NATURAL_32; v: NATURAL_32; w: NATURAL_32): NATURAL_32 is
do
result := u.bit_xor (v).bit_xor (w)
end
feature {NONE} -- Padding facilities
pad
local
pad_bytes: INTEGER_32
do
update (0b1000_0000)
from
pad_bytes := (56 - (byte_count \\ 64)).to_integer_32
if
pad_bytes < 0
then
pad_bytes := pad_bytes + 64
end
until
pad_bytes = 0
loop
update (0)
pad_bytes := pad_bytes - 1
end
end
byte_count: NATURAL_64
bit_count: NATURAL_64
do
result := byte_count |<< 3
end
update (in: NATURAL_8)
do
precursor (in)
byte_count := byte_count + 1
ensure then
byte_count = old byte_count + 1
end
feature {NONE} -- Length processing facilities
process_length (length: NATURAL_64)
require
schedule_start: schedule_offset = 14
empty_buffer: buffer_offset = 0
do
update_word ((length |>> 32).to_natural_32)
update_word (length.to_natural_32)
ensure
empty_buffer: buffer_offset = 0
schedule_end: schedule_offset = 0
end
process_word (in: SPECIAL [NATURAL_8]; offset: INTEGER_32)
do
schedule [schedule_offset] := as_natural_32_be (in, offset)
schedule_offset := schedule_offset + 1
if
schedule_offset = 16
then
schedule_offset := 0
process_block
end
end
process_block
deferred
end
finish is
local
length: NATURAL_64
do
length := bit_count
pad
process_length (length)
end
feature {NONE}
schedule: SPECIAL [NATURAL_32]
schedule_offset: INTEGER_32
invariant
valid_schedule_offset: schedule.valid_index (schedule_offset)
valid_schedule_offset_lower: schedule_offset >= 0
valid_schedule_offset_upper: schedule_offset <= 15
valid_schedule_lower: schedule.valid_index (0)
valid_schedule_upper: schedule.valid_index (15)
end