From 0209586ac22efe9cb87432832793c3eb5857620b Mon Sep 17 00:00:00 2001 From: Karthikeyan Bhargavan Date: Mon, 30 Oct 2023 11:59:06 +0100 Subject: [PATCH] digest interface --- proofs/fstar/extraction/Libcrux.Digest.fst | 6 ---- proofs/fstar/extraction/Libcrux.Digest.fsti | 39 +++++++++++++++++++++ 2 files changed, 39 insertions(+), 6 deletions(-) delete mode 100644 proofs/fstar/extraction/Libcrux.Digest.fst create mode 100644 proofs/fstar/extraction/Libcrux.Digest.fsti diff --git a/proofs/fstar/extraction/Libcrux.Digest.fst b/proofs/fstar/extraction/Libcrux.Digest.fst deleted file mode 100644 index 0cd21372e..000000000 --- a/proofs/fstar/extraction/Libcrux.Digest.fst +++ /dev/null @@ -1,6 +0,0 @@ -module Libcrux.Digest - -open Rust_primitives - -type alg = | Algorithm_Sha3_256_ -let digest_size x = sz 32 diff --git a/proofs/fstar/extraction/Libcrux.Digest.fsti b/proofs/fstar/extraction/Libcrux.Digest.fsti new file mode 100644 index 000000000..2df30e7d8 --- /dev/null +++ b/proofs/fstar/extraction/Libcrux.Digest.fsti @@ -0,0 +1,39 @@ +module Libcrux.Digest +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Rust_primitives +open Core + +type t_Algorithm = + | Algorithm_Sha1 : t_Algorithm + | Algorithm_Sha224 : t_Algorithm + | Algorithm_Sha256 : t_Algorithm + | Algorithm_Sha384 : t_Algorithm + | Algorithm_Sha512 : t_Algorithm + | Algorithm_Blake2s : t_Algorithm + | Algorithm_Blake2b : t_Algorithm + | Algorithm_Sha3_224_ : t_Algorithm + | Algorithm_Sha3_256_ : t_Algorithm + | Algorithm_Sha3_384_ : t_Algorithm + | Algorithm_Sha3_512_ : t_Algorithm + +let digest_size (mode: t_Algorithm) : usize = + match mode with + | Algorithm_Sha1 -> sz 20 + | Algorithm_Sha224 -> sz 28 + | Algorithm_Sha256 -> sz 32 + | Algorithm_Sha384 -> sz 48 + | Algorithm_Sha512 -> sz 64 + | Algorithm_Blake2s -> sz 32 + | Algorithm_Blake2b -> sz 64 + | Algorithm_Sha3_224_ -> sz 28 + | Algorithm_Sha3_256_ -> sz 32 + | Algorithm_Sha3_384_ -> sz 48 + | Algorithm_Sha3_512_ -> sz 64 + +val sha3_256_ (payload: t_Slice u8) : t_Array u8 (sz 32) + +val sha3_512_ (payload: t_Slice u8) : t_Array u8 (sz 64) + +val shake128 (#v_LEN: usize) (data: t_Slice u8) : t_Array u8 v_LEN + +val shake256 (#v_LEN: usize) (data: t_Slice u8) : t_Array u8 v_LEN