let v' (#a: sha2_alg) (x:word a) = match a with
  | SHA2_224 | SHA2_256 -> uint_v #U32 #SEC x
  | SHA2_384 | SHA2_512 -> uint_v #U64 #SEC x
let v' (#a: sha2_alg) (x: word a) =
match a with
| SHA2_224 | SHA2_256 -> uint_v #U32 #SEC x
| SHA2_384 | SHA2_512 -> uint_v #U64 #SEC x
Spec.SHA2.fst.checked
Spec.SHA2.Constants.fst.checked Spec.Loops.fst.checked Spec.Hash.Definitions.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Spec.SHA2.fst
Spec.Hash.Definitions.sha2_alg Spec.Hash.Definitions.word Lib.IntTypes.uint_v Lib.IntTypes.U32 Lib.IntTypes.SEC Lib.IntTypes.U64 Prims.int Prims.l_or Lib.IntTypes.range
module Spec.SHA2

open Lib.IntTypes
module C = Spec.SHA2.Constants
module S = FStar.Seq

open Spec.Hash.Definitions

(* The core compression, padding and extraction functions for all SHA2
 * algorithms. *)

(* Define the length of the constants. Also the number of scheduling rounds. *)
inline_for_extraction
let size_k_w: sha2_alg -> Tot nat = function
  | SHA2_224 | SHA2_256 -> 64
  | SHA2_384 | SHA2_512 -> 80

inline_for_extraction
let word_n: sha2_alg -> Tot nat = function
  | SHA2_224 | SHA2_256 -> 32
  | SHA2_384 | SHA2_512 -> 64

inline_for_extraction
let to_word (a:sha2_alg) (n:nat{n < pow2 (word_n a)}) : word a =
  match a with
  | SHA2_224 | SHA2_256 -> u32 n
  | SHA2_384 | SHA2_512 -> u64 n
val v' : x: Spec.Hash.Definitions.word a
  -> x:
    Prims.int
      { Lib.IntTypes.range x Lib.IntTypes.U32 \/ Lib.IntTypes.range x Lib.IntTypes.U64 \/
        Lib.IntTypes.range x Lib.IntTypes.U64 \/ Lib.IntTypes.range x Lib.IntTypes.U32 }
x: Spec.Hash.Definitions.word a
  -> x:
    Prims.int
      { Lib.IntTypes.range x Lib.IntTypes.U32 \/ Lib.IntTypes.range x Lib.IntTypes.U64 \/
        Lib.IntTypes.range x Lib.IntTypes.U64 \/ Lib.IntTypes.range x Lib.IntTypes.U32 }