1#![no_std]
6#![forbid(unsafe_code)]
7#![deny(missing_docs)]
8
9mod simd;
10
11mod generic_keccak;
12
13#[cfg(not(any(hax, eurydice)))]
14mod impl_digest_trait;
15#[cfg(not(any(hax, eurydice)))]
16pub use impl_digest_trait::*;
17
18#[cfg(hax)]
19use hax_lib::int::*;
20
21mod traits;
22
23pub const SHA3_224_DIGEST_SIZE: usize = 28;
25pub const SHA3_256_DIGEST_SIZE: usize = 32;
27pub const SHA3_384_DIGEST_SIZE: usize = 48;
29pub const SHA3_512_DIGEST_SIZE: usize = 64;
31
32#[cfg(hax)]
34pub(crate) mod proof_utils;
35
36#[cfg_attr(not(eurydice), derive(Debug, PartialEq))]
38#[derive(Clone, Copy)]
39#[repr(u32)]
40pub enum Algorithm {
41 Sha224 = 1,
43
44 Sha256 = 2,
46
47 Sha384 = 3,
49
50 Sha512 = 4,
52}
53
54#[cfg(not(any(hax, eurydice)))]
56impl From<u32> for Algorithm {
57 fn from(v: u32) -> Algorithm {
58 match v {
59 1 => Algorithm::Sha224,
60 2 => Algorithm::Sha256,
61 3 => Algorithm::Sha384,
62 4 => Algorithm::Sha512,
63 _ => panic!("Invalid SHA3 Algorithm code"),
64 }
65 }
66}
67
68impl From<Algorithm> for u32 {
69 fn from(v: Algorithm) -> u32 {
70 match v {
71 Algorithm::Sha224 => 1,
72 Algorithm::Sha256 => 2,
73 Algorithm::Sha384 => 3,
74 Algorithm::Sha512 => 4,
75 }
76 }
77}
78
79pub const fn digest_size(mode: Algorithm) -> usize {
81 match mode {
82 Algorithm::Sha224 => SHA3_224_DIGEST_SIZE,
83 Algorithm::Sha256 => SHA3_256_DIGEST_SIZE,
84 Algorithm::Sha384 => SHA3_384_DIGEST_SIZE,
85 Algorithm::Sha512 => SHA3_512_DIGEST_SIZE,
86 }
87}
88
89#[hax_lib::fstar::options("--split_queries always")]
91#[hax_lib::requires(
92 payload.len().to_int() <= u32::MAX.to_int() &&
93 digest_size(algorithm) == LEN
94)]
95pub fn hash<const LEN: usize>(algorithm: Algorithm, payload: &[u8]) -> [u8; LEN] {
96 debug_assert!(payload.len() <= u32::MAX as usize);
97 debug_assert_eq!(digest_size(algorithm), LEN);
98
99 let mut out = [0u8; LEN];
100 match algorithm {
101 Algorithm::Sha224 => portable::sha224(&mut out, payload),
102 Algorithm::Sha256 => portable::sha256(&mut out, payload),
103 Algorithm::Sha384 => portable::sha384(&mut out, payload),
104 Algorithm::Sha512 => portable::sha512(&mut out, payload),
105 }
106 out
107}
108
109pub use hash as sha3;
111
112#[cfg_attr(not(eurydice), inline(always))]
114#[hax_lib::requires(
115 data.len().to_int() <= u32::MAX.to_int()
116)]
117pub fn sha224(data: &[u8]) -> [u8; SHA3_224_DIGEST_SIZE] {
118 let mut out = [0u8; SHA3_224_DIGEST_SIZE];
119 sha224_ema(&mut out, data);
120 out
121}
122
123#[cfg_attr(not(eurydice), inline(always))]
128#[hax_lib::requires(
129 payload.len().to_int() <= u32::MAX.to_int() &&
130 digest.len().to_int() == int!(28)
131)]
132pub fn sha224_ema(digest: &mut [u8], payload: &[u8]) {
133 debug_assert!(payload.len() <= u32::MAX as usize);
134 debug_assert!(digest.len() == 28);
135
136 portable::sha224(digest, payload)
137}
138
139#[cfg_attr(not(eurydice), inline(always))]
141#[hax_lib::requires(
142 data.len().to_int() <= u32::MAX.to_int()
143)]
144pub fn sha256(data: &[u8]) -> [u8; SHA3_256_DIGEST_SIZE] {
145 let mut out = [0u8; SHA3_256_DIGEST_SIZE];
146 sha256_ema(&mut out, data);
147 out
148}
149
150#[cfg_attr(not(eurydice), inline(always))]
152#[hax_lib::requires(
153 payload.len().to_int() <= u32::MAX.to_int() &&
154 digest.len().to_int() == int!(32)
155)]
156pub fn sha256_ema(digest: &mut [u8], payload: &[u8]) {
157 debug_assert!(payload.len() <= u32::MAX as usize);
158 debug_assert!(digest.len() == 32);
159
160 portable::sha256(digest, payload)
161}
162
163#[cfg_attr(not(eurydice), inline(always))]
165#[hax_lib::requires(
166 data.len().to_int() <= u32::MAX.to_int()
167)]
168pub fn sha384(data: &[u8]) -> [u8; SHA3_384_DIGEST_SIZE] {
169 let mut out = [0u8; SHA3_384_DIGEST_SIZE];
170 sha384_ema(&mut out, data);
171 out
172}
173
174#[cfg_attr(not(eurydice), inline(always))]
176#[hax_lib::requires(
177 payload.len().to_int() <= u32::MAX.to_int() &&
178 digest.len().to_int() == int!(48)
179)]
180pub fn sha384_ema(digest: &mut [u8], payload: &[u8]) {
181 debug_assert!(payload.len() <= u32::MAX as usize);
182 debug_assert!(digest.len() == 48);
183
184 portable::sha384(digest, payload)
185}
186
187#[cfg_attr(not(eurydice), inline(always))]
189#[hax_lib::requires(
190 data.len().to_int() <= u32::MAX.to_int()
191)]
192pub fn sha512(data: &[u8]) -> [u8; SHA3_512_DIGEST_SIZE] {
193 let mut out = [0u8; SHA3_512_DIGEST_SIZE];
194 sha512_ema(&mut out, data);
195 out
196}
197
198#[cfg_attr(not(eurydice), inline(always))]
200#[hax_lib::requires(
201 payload.len().to_int() <= u32::MAX.to_int() &&
202 digest.len().to_int() == int!(64)
203)]
204pub fn sha512_ema(digest: &mut [u8], payload: &[u8]) {
205 debug_assert!(payload.len() <= u32::MAX as usize);
206 debug_assert!(digest.len() == 64);
207
208 portable::sha512(digest, payload)
209}
210
211#[cfg_attr(not(eurydice), inline(always))]
216pub fn shake128<const BYTES: usize>(data: &[u8]) -> [u8; BYTES] {
217 let mut out = [0u8; BYTES];
218 portable::shake128(&mut out, data);
219 out
220}
221
222#[cfg_attr(not(eurydice), inline(always))]
226pub fn shake128_ema(out: &mut [u8], data: &[u8]) {
227 portable::shake128(out, data);
228}
229
230#[cfg_attr(not(eurydice), inline(always))]
235pub fn shake256<const BYTES: usize>(data: &[u8]) -> [u8; BYTES] {
236 let mut out = [0u8; BYTES];
237 portable::shake256(&mut out, data);
238 out
239}
240
241#[cfg_attr(not(eurydice), inline(always))]
245pub fn shake256_ema(out: &mut [u8], data: &[u8]) {
246 portable::shake256(out, data);
247}
248
249pub mod portable;
253
254#[cfg(feature = "simd128")]
262pub mod neon;
263
264#[cfg(feature = "simd256")]
272pub mod avx2;