https://github.com/project-everest/hacl-star
Raw File
Tip revision: 584233f24975d55dd131542cc81930c231f93ed6 authored by Aymeric Fromherz on 02 July 2021, 04:14:39 UTC
Expand list of supported algorithms in doc
Tip revision: 584233f
Hacl.Hash.Agile.fst
module Hacl.Hash.Agile

open Hacl.Hash.Definitions
open Spec.Hash.Definitions

(** A series of static multiplexers that will be useful when building the
    generic Merkle-Damgard construction. *)

inline_for_extraction noextract
let alloca (i:impl): alloca_st i =
  [@inline_let] let a = get_alg i in
  [@inline_let] let m = get_spec i in
  match a with
  | MD5 -> Hacl.Hash.Core.MD5.legacy_alloca
  | SHA1 -> Hacl.Hash.Core.SHA1.legacy_alloca
  | SHA2_224 -> Hacl.Hash.Core.SHA2.alloca_224
  | SHA2_256 -> Hacl.Hash.Core.SHA2.alloca_256
  | SHA2_384 -> Hacl.Hash.Core.SHA2.alloca_384
  | SHA2_512 -> Hacl.Hash.Core.SHA2.alloca_512
  | Blake2S -> Hacl.Hash.Core.Blake2.mk_alloca Blake2S m (Hacl.Hash.Core.Blake2.mk_init Blake2S m)
  | Blake2B -> Hacl.Hash.Core.Blake2.mk_alloca Blake2B m (Hacl.Hash.Core.Blake2.mk_init Blake2B m)

inline_for_extraction noextract
let init (i:impl): init_st i =
  [@inline_let] let a = get_alg i in
  [@inline_let] let m = get_spec i in
  match a with
  | MD5 -> Hacl.Hash.Core.MD5.legacy_init
  | SHA1 -> Hacl.Hash.Core.SHA1.legacy_init
  | SHA2_224 -> Hacl.Hash.Core.SHA2.init_224
  | SHA2_256 -> Hacl.Hash.Core.SHA2.init_256
  | SHA2_384 -> Hacl.Hash.Core.SHA2.init_384
  | SHA2_512 -> Hacl.Hash.Core.SHA2.init_512
  | Blake2S -> Hacl.Hash.Core.Blake2.mk_init Blake2S m
  | Blake2B -> Hacl.Hash.Core.Blake2.mk_init Blake2B m


inline_for_extraction noextract
let update (i:impl): update_st i =
  [@inline_let] let a = get_alg i in
  [@inline_let] let m = get_spec i in
  match a with
  | MD5 -> Hacl.Hash.Core.MD5.legacy_update
  | SHA1 -> Hacl.Hash.Core.SHA1.legacy_update
  | SHA2_224 -> Hacl.Hash.Core.SHA2.update_224
  | SHA2_256 -> Hacl.Hash.Core.SHA2.update_256
  | SHA2_384 -> Hacl.Hash.Core.SHA2.update_384
  | SHA2_512 -> Hacl.Hash.Core.SHA2.update_512
  | Blake2S -> Hacl.Hash.Core.Blake2.mk_update Blake2S m
  | Blake2B -> Hacl.Hash.Core.Blake2.mk_update Blake2B m

inline_for_extraction noextract
let pad (a: hash_alg): pad_st a =
  match a with
  | MD5 -> Hacl.Hash.Core.MD5.legacy_pad
  | SHA1 -> Hacl.Hash.Core.SHA1.legacy_pad
  | SHA2_224 -> Hacl.Hash.Core.SHA2.pad_224
  | SHA2_256 -> Hacl.Hash.Core.SHA2.pad_256
  | SHA2_384 -> Hacl.Hash.Core.SHA2.pad_384
  | SHA2_512 -> Hacl.Hash.Core.SHA2.pad_512
  | Blake2S -> Hacl.Hash.Core.Blake2.pad_blake2s
  | Blake2B -> Hacl.Hash.Core.Blake2.pad_blake2b

inline_for_extraction noextract
let finish (i:impl): finish_st i =
  [@inline_let] let a = get_alg i in
  [@inline_let] let m = get_spec i in
  match a with
  | MD5 -> Hacl.Hash.Core.MD5.legacy_finish
  | SHA1 -> Hacl.Hash.Core.SHA1.legacy_finish
  | SHA2_224 -> Hacl.Hash.Core.SHA2.finish_224
  | SHA2_256 -> Hacl.Hash.Core.SHA2.finish_256
  | SHA2_384 -> Hacl.Hash.Core.SHA2.finish_384
  | SHA2_512 -> Hacl.Hash.Core.SHA2.finish_512
  | Blake2S -> Hacl.Hash.Core.Blake2.mk_finish Blake2S m
  | Blake2B -> Hacl.Hash.Core.Blake2.mk_finish Blake2B m
back to top