val word_n: sha2_alg -> Tot nat
let word_n: sha2_alg -> Tot nat = function
  | SHA2_224 | SHA2_256 -> 32
  | SHA2_384 | SHA2_512 -> 64
val word_n: sha2_alg -> Tot nat
let word_n: sha2_alg -> Tot nat =
function
| SHA2_224 | SHA2_256 -> 32
| SHA2_384 | SHA2_512 -> 64
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 Prims.nat
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
val word_n: sha2_alg -> Tot nat
_: Spec.Hash.Definitions.sha2_alg -> Prims.nat