val byte_sec : Type0
let byte_sec = uint8
module L0.Base

open LowStar.Comment

module Fail = LowStar.Failure
module B = LowStar.Buffer
module IB = LowStar.ImmutableBuffer
module HS  = FStar.HyperStack
module HST = FStar.HyperStack.ST

module SHA2 = Hacl.Hash.SHA2
module HMAC = Hacl.HMAC
module HKDF = Hacl.HKDF
// module ECDSA = Hacl.Impl.ECDSA
// module P256 = Hacl.Impl.P256
module Ed25519 = Hacl.Ed25519
module Curve25519 = Hacl.Curve25519_51

// module HW = HWAbstraction
open L0.Declassify
open Lib.IntTypes
open Spec.Hash.Definitions
open Hacl.Hash.Definitions
(*
 * Some common definitions used in the L0 code
 *)

inline_for_extraction noextract
let l0_hash_alg = a:hash_alg{a == SHA2_256}

inline_for_extraction noextract
let alg : l0_hash_alg = SHA2_256

inline_for_extraction noextract
let l0_hash (alg:l0_hash_alg) : hash_st alg =
  match alg with
  | SHA2_256 -> Hacl.Streaming.SHA2.hash_256
  | SHA2_384 -> Hacl.Streaming.SHA2.hash_384
  | SHA2_512 -> Hacl.Streaming.SHA2.hash_512
  // | SHA1     -> Hacl.Hash.SHA1.legacy_hash

inline_for_extraction noextract
let l0_hmac (alg:l0_hash_alg) : Hacl.HMAC.compute_st alg =
  match alg with
  | SHA2_256 -> Hacl.HMAC.compute_sha2_256
  | SHA2_384 -> Hacl.HMAC.compute_sha2_384
  | SHA2_512 -> Hacl.HMAC.compute_sha2_512
  // | SHA1     -> Hacl.HMAC.legacy_compute_sha1

unfold noextract let digest_len = hash_len alg

unfold noextract type digest_t = hash_t alg

unfold noextract type hashable_len = i:size_t{0 < v i /\ v i <= (Some?.v (max_input_length alg))}

unfold noextract let cdi_len = digest_len
/
Spec.Hash.Definitions.fst.checked prims.fst.checked LowStar.ImmutableBuffer.fst.checked LowStar.Failure.fsti.checked LowStar.Comment.fsti.checked LowStar.Buffer.fst.checked Lib.IntTypes.fsti.checked L0.Declassify.fsti.checked Hacl.Streaming.SHA2.fst.checked Hacl.HMAC.fsti.checked Hacl.HKDF.fsti.checked Hacl.Hash.SHA2.fsti.checked Hacl.Hash.Definitions.fst.checked Hacl.Ed25519.fsti.checked Hacl.Curve25519_51.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
L0.Base.fst
Type0
Lib.IntTypes.uint8
let byte_sec =
  
uint8